diff options
| author | Christian Doczkal | 2019-11-03 16:33:44 +0100 |
|---|---|---|
| committer | Christian Doczkal | 2019-11-04 11:10:11 +0100 |
| commit | 185ea5895b1e89eaf6f741d560910a24541c62eb (patch) | |
| tree | 2c9777877570aefa1af34d65762dbdcfe3cf7720 /mathcomp/field | |
| parent | 71e397e46b65c1c27a65471170d71f388c8a45f1 (diff) | |
add existsPn/forallPn lemmas
Diffstat (limited to 'mathcomp/field')
| -rw-r--r-- | mathcomp/field/galois.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/field/galois.v b/mathcomp/field/galois.v index 30bef47..14bba86 100644 --- a/mathcomp/field/galois.v +++ b/mathcomp/field/galois.v @@ -1352,7 +1352,7 @@ rewrite ltnS (cardD1x Px) in lePn; move/IHn: lePn => {n IHn}/=IH_P. have [/eqfun_inP c_Px'_0 | ] := boolP [forall (y | P y && (y != x)), c_ y == 0]. exists 1; rewrite ?mem1v // (bigD1 x Px) /= rmorph1 mulr1. by rewrite big1 ?addr0 // => y /c_Px'_0->; rewrite mul0r. -rewrite negb_forall_in => /exists_inP[y Px'y nz_cy]. +case/forall_inPn => y Px'y nz_cy. have [Py /gal_eqP/eqlfun_inP/subvPn[a Ea]] := andP Px'y. rewrite memv_ker !lfun_simp => nz_yxa; pose d_ y := c_ y * (y a - x a). have /IH_P[//|b Eb nz_sumb]: d_ y != 0 by rewrite mulf_neq0. |