Explicit `bigop` enumeration handling

Added lemmas `big_enum_cond`, `big_enum` and `big_enumP` to handle more
explicitly big ops iterating over explicit enumerations in a `finType`.
   The previous practice was to rely on the convertibility between
`enum A` and `filter A (index_enum T)`, sometimes explicitly via the
`filter_index_enum` equality, more often than not implicitly.
  Both are likely to fail after the integration of `finmap`, as the
`choiceType` theory can’t guarantee that the order in selected
enumerations is consistent.
  For this reason `big_enum` and the related (but currently unused)
`big_image` lemmas are restricted to the abelian case. The `big_enumP`
lemma can be used to handle enumerations in the non-abelian case, as
explained in the `bigop.v` internal documentation.
  The Changelog entry enjoins clients to stop relying on either
`filter_index_enum` and convertibility (though this PR still provides
both), and warns about the restriction of the `big_image` lemma set to
the abelian case, as it it a possible source of incompatibility.

1 files changed, 1 insertions, 1 deletions

diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v
index 38beffc..7e1dfbb 100644
--- a/mathcomp/algebra/mxalgebra.v
+++ b/mathcomp/algebra/mxalgebra.v
@@ -2091,7 +2091,7 @@ Lemma mxdirect_delta n f : {in P &, injective f} ->
 Proof.
 pose fP := image f P => Uf; have UfP: uniq fP by apply/dinjectiveP.
 suffices /mxdirectP : mxdirect (\sum_i <<delta_mx 0 i : 'rV[F]_n>>).
-  rewrite /= !(bigID [mem fP] predT) -!big_uniq //= !big_map !big_filter.
+  rewrite /= !(bigID [mem fP] predT) -!big_uniq //= !big_map !big_enum.
   by move/mxdirectP; rewrite mxdirect_addsE => /andP[].
 apply/mxdirectP=> /=; transitivity (mxrank (1%:M : 'M[F]_n)).
   apply/eqmx_rank; rewrite submx1 mx1_sum_delta summx_sub_sums // => i _.