diff options
| author | Cyril Cohen | 2019-11-06 15:54:03 +0100 |
|---|---|---|
| committer | GitHub | 2019-11-06 15:54:03 +0100 |
| commit | 9a8b8292371526978b9e34804daf114658fe4b7a (patch) | |
| tree | af3b6de4ec0b11f970d699943373af6894fe7115 /mathcomp/field | |
| parent | fcffe720b5a66bb6c0d9b6179dbef2b7af8805b6 (diff) | |
| parent | ad84fa64677463ab27a10bcd4d0081fd06693945 (diff) | |
Merge pull request #408 from chdoc/existsPn
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 9a2bdfd..7937a24 100644 --- a/mathcomp/field/galois.v +++ b/mathcomp/field/galois.v @@ -1358,7 +1358,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. |