diff options
| author | Cyril Cohen | 2020-09-01 15:44:13 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2020-09-03 19:59:28 +0200 |
| commit | fbeec199e65fe7e9fd96ddd74e31aa0461c22927 (patch) | |
| tree | bff3b089214e20c21a63b053670793a7bf44fe91 /mathcomp/field | |
| parent | 495919767802fea4089594726d585c9b5305df21 (diff) | |
Lemmas reindex_omap and bigD1_ord
+ eq_liftF and lift_eqF
+ proof simplificaions
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). |