diff options
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). |