diff options
| author | Laurent Théry | 2020-09-04 12:14:00 +0200 |
|---|---|---|
| committer | GitHub | 2020-09-04 12:14:00 +0200 |
| commit | d693784678f8a1889fdc3731587f31dc7c9377ff (patch) | |
| tree | 413e131d444270f9d993437f13122e4aa5bc4277 /mathcomp/field | |
| parent | 495919767802fea4089594726d585c9b5305df21 (diff) | |
| parent | 667dd52bd039a96f896b81533b0aaafe98b9f8de (diff) | |
Merge pull request #572 from CohenCyril/reindex_omap
Lemmas reindex_omap and bigD1_ord
Diffstat (limited to 'mathcomp/field')
| -rw-r--r-- | mathcomp/field/algnum.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mathcomp/field/algnum.v b/mathcomp/field/algnum.v index 997255b..821a21e 100644 --- a/mathcomp/field/algnum.v +++ b/mathcomp/field/algnum.v @@ -150,8 +150,8 @@ Lemma mem_Crat_span s : {subset s <= Crat_span s}. Proof. move=> _ /(nthP 0)[ix ltxs <-]; pose i0 := Ordinal ltxs. apply/Crat_spanP; exists [ffun i => (i == i0)%:R]. -rewrite (bigD1 i0) //= ffunE eqxx // rmorph1 mul1r. -by rewrite big1 ?addr0 // => i; rewrite ffunE rmorph_nat mulr_natl => /negbTE->. +rewrite (bigD1_ord i0) //= ffunE eqxx // rmorph1 mul1r. +by rewrite big1 ?addr0 // => i; rewrite ffunE rmorph_nat mulr_natl lift_eqF. Qed. Fact Crat_span_zmod_closed s : zmod_closed (Crat_span s). |