diff options
Diffstat (limited to 'mathcomp/field')
| -rw-r--r-- | mathcomp/field/algebraics_fundamentals.v | 10 | ||||
| -rw-r--r-- | mathcomp/field/closed_field.v | 13 | ||||
| -rw-r--r-- | mathcomp/field/cyclotomic.v | 11 | ||||
| -rw-r--r-- | mathcomp/field/falgebra.v | 4 | ||||
| -rw-r--r-- | mathcomp/field/fieldext.v | 27 | ||||
| -rw-r--r-- | mathcomp/field/separable.v | 34 |
6 files changed, 47 insertions, 52 deletions
diff --git a/mathcomp/field/algebraics_fundamentals.v b/mathcomp/field/algebraics_fundamentals.v index d8ad524..a950ecc 100644 --- a/mathcomp/field/algebraics_fundamentals.v +++ b/mathcomp/field/algebraics_fundamentals.v @@ -160,7 +160,7 @@ have [n ub_n]: {n | forall y, root q y -> `|y| < n}. have [n1 ub_n1] := monic_Cauchy_bound mon_q. have /monic_Cauchy_bound[n2 ub_n2]: (-1) ^+ d *: (q \Po - 'X) \is monic. rewrite monicE lead_coefZ lead_coef_comp ?size_opp ?size_polyX // -/d. - by rewrite lead_coef_opp lead_coefX (monicP mon_q) (mulrC 1) signrMK. + by rewrite lead_coefN lead_coefX (monicP mon_q) (mulrC 1) signrMK. exists (Num.max n1 n2) => y; rewrite ltNge ler_normr !leUx rootE. apply: contraL => /orP[]/andP[] => [/ub_n1/gt_eqF->// | _ /ub_n2/gt_eqF]. by rewrite hornerZ horner_comp !hornerE opprK mulf_eq0 signr_eq0 => /= ->. @@ -171,7 +171,7 @@ right=> [[y Dx]]; case: xa'x; exists y => //. have{x Dx qx0} qy0: root q y by rewrite Dx fmorph_root in qx0. have /dvdzP[b Da]: (denq y %| a)%Z. have /Gauss_dvdzl <-: coprimez (denq y) (numq y ^+ d). - by rewrite coprimez_sym coprimez_expl //; apply: coprime_num_den. + by rewrite coprimez_sym coprimezXl //; apply: coprime_num_den. pose p1 : {poly int} := a *: 'X^d - p. have Dp1: p1 ^ intr = a%:~R *: ('X^d - q). by rewrite rmorphB linearZ /= map_polyXn scalerBr Dq scalerKV ?intr_eq0. @@ -231,7 +231,7 @@ without loss mon_q: q nCq q_dv_p / q \is monic. move=> IHq; pose a := lead_coef q; pose q1 := a^-1 *: q. have nz_a: a != 0 by rewrite lead_coef_eq0 (dvdpN0 q_dv_p) ?monic_neq0. have /IHq IHq1: q1 \is monic by rewrite monicE lead_coefZ mulVf. - by rewrite -IHq1 ?size_scale ?dvdp_scalel ?invr_eq0. + by rewrite -IHq1 ?size_scale ?dvdpZl ?invr_eq0. without loss{nCq} qx0: q mon_q q_dv_p / root (q ^ FtoL) x. have /dvdpP[q1 Dp] := q_dv_p; rewrite DpI Dp rmorphM rootM -implyNb in pIx0. have mon_q1: q1 \is monic by rewrite Dp monicMr in mon_p. @@ -515,7 +515,7 @@ have add_Rroot xR p c: {yR | extendsR xR yR & has_Rroot xR p c -> root_in yR p}. have ab_le m n: (m <= n)%N -> (ab_ n).2 \in Iab_ m. move/subnKC=> <-; move: {n}(n - m)%N => n; rewrite /ab_. have /(findP m)[/(findP n)[[_ _]]] := xab0. - rewrite /find -iter_add -!/(find _ _) -!/(ab_ _) addnC !inE. + rewrite /find -iterD -!/(find _ _) -!/(ab_ _) addnC !inE. by move: (ab_ _) => /= ab_mn le_ab_mn [/le_trans->]. pose lt v w := 0 < nlim (w - v) (n_ (w - v)). have posN v: lt 0 (- v) = lt v 0 by rewrite /lt subr0 add0r. @@ -723,7 +723,7 @@ have /all_sig[n_ FTA] z: {n | z \in sQ (z_ n)}. have mon_p: p \is monic. have mon_pw: pw \is monic := monic_minPoly _ _. rewrite map_monic mulNr -mulrN monicMl // monicE. - rewrite !(lead_coef_opp, lead_coef_comp) ?size_opp ?size_polyX //. + rewrite !(lead_coefN, lead_coef_comp) ?size_opp ?size_polyX //. by rewrite lead_coefX sz_pw -signr_odd odd_2'nat oddPG mulrN1 opprK. have Dp0: p.[0] = - ofQ t pw.[0] ^+ 2. rewrite -(rmorph0 (ofQ t)) horner_map hornerM rmorphM. diff --git a/mathcomp/field/closed_field.v b/mathcomp/field/closed_field.v index a6f7514..266788c 100644 --- a/mathcomp/field/closed_field.v +++ b/mathcomp/field/closed_field.v @@ -200,7 +200,7 @@ Lemma eval_sumpT (p q : polyF) (e : seq F) : Proof. elim: p q => [|a p Hp] q /=; first by rewrite add0r. case: q => [|b q] /=; first by rewrite addr0. -rewrite Hp mulrDl -!addrA; congr (_ + _); rewrite polyC_add addrC -addrA. +rewrite Hp mulrDl -!addrA; congr (_ + _); rewrite polyCD addrC -addrA. by congr (_ + _); rewrite addrC. Qed. @@ -220,15 +220,12 @@ Lemma eval_mulpT (p q : polyF) (e : seq F) : Proof. elim: p q=> [|a p Hp] q /=; first by rewrite mul0r. rewrite eval_sumpT /= Hp addr0 mulrDl addrC mulrAC; congr (_ + _). -elim: q=> [|b q Hq] /=; first by rewrite mulr0. -by rewrite Hq polyC_mul mulrDr mulrA. +by elim: q=> [|b q Hq] /=; rewrite ?mulr0 // Hq polyCM mulrDr mulrA. Qed. Lemma rpoly_map_mul (t : tF) (p : polyF) (rt : rterm t) : rpoly [seq (t * x)%T | x <- p] = rpoly p. -Proof. -by rewrite /rpoly all_map /= (@eq_all _ _ (@rterm _)) // => x; rewrite /= rt. -Qed. +Proof. by rewrite /rpoly all_map; apply/eq_all => x; rewrite /= rt. Qed. Lemma rmulpT (p q : polyF) : rpoly p -> rpoly q -> rpoly (mulpT p q). Proof. @@ -242,7 +239,7 @@ Definition opppT : polyF -> polyF := map (GRing.Mul (- 1%T)%T). Lemma eval_opppT (p : polyF) (e : seq F) : eval_poly e (opppT p) = - eval_poly e p. Proof. -by elim: p; rewrite /= ?oppr0 // => ? ? ->; rewrite !mulNr opprD polyC_opp mul1r. +by elim: p; rewrite /= ?oppr0 // => ? ? ->; rewrite !mulNr opprD polyCN mul1r. Qed. Definition natmulpT n : polyF -> polyF := map (GRing.Mul n%:R%T). @@ -251,7 +248,7 @@ Lemma eval_natmulpT (p : polyF) (n : nat) (e : seq F) : eval_poly e (natmulpT n p) = (eval_poly e p) *+ n. Proof. elim: p; rewrite //= ?mul0rn // => c p ->. -rewrite mulrnDl mulr_natl polyC_muln; congr (_ + _). +rewrite mulrnDl mulr_natl polyCMn; congr (_ + _). by rewrite -mulr_natl mulrAC -mulrA mulr_natl mulrC. Qed. diff --git a/mathcomp/field/cyclotomic.v b/mathcomp/field/cyclotomic.v index 658258c..5359cce 100644 --- a/mathcomp/field/cyclotomic.v +++ b/mathcomp/field/cyclotomic.v @@ -50,10 +50,9 @@ End Ring. Lemma separable_Xn_sub_1 (R : idomainType) n : n%:R != 0 :> R -> @separable_poly R ('X^n - 1). Proof. -case: n => [/eqP// | n nz_n]; rewrite /separable_poly linearB /=. -rewrite derivC subr0 derivXn -scaler_nat coprimep_scaler //= exprS -scaleN1r. -rewrite coprimep_sym coprimep_addl_mul coprimep_scaler ?coprimep1 //. -by rewrite (signr_eq0 _ 1). +case: n => [/eqP// | n nz_n]; rewrite /separable_poly linearB /= derivC subr0. +rewrite derivXn -scaler_nat coprimepZr //= exprS -scaleN1r coprimep_sym. +by rewrite coprimep_addl_mul coprimepZr ?coprimep1 // (signr_eq0 _ 1). Qed. Section Field. @@ -188,7 +187,7 @@ have injf: injective (f e). rewrite modnMml -mulnA -modnMmr -{1}(mul1n e). by rewrite (chinese_modr co_e_n 0) modnMmr muln1 modn_small. rewrite [_ n](reindex_inj injf); apply: eq_big => k /=. - by rewrite coprime_modl coprime_mull co_e_n andbT. + by rewrite coprime_modl coprimeMl co_e_n andbT. by rewrite prim_expr_mod // mulnC exprM -Dz0. Qed. @@ -269,7 +268,7 @@ have [|k_gt1] := leqP k 1; last have [p p_pr /dvdnP[k1 Dk]] := pdivP k_gt1. rewrite k0 /coprime gcd0n in cokn; rewrite (eqP cokn). rewrite -(size_map_inj_poly (can_inj intCK)) // -Df -Dpf. by rewrite -(subnKC g_gt1) -(subnKC (size_minCpoly z)) !addnS. -move: cokn; rewrite Dk coprime_mull => /andP[cok1n]. +move: cokn; rewrite Dk coprimeMl => /andP[cok1n]. rewrite prime_coprime // (dvdn_charf (char_Fp p_pr)) => /co_fg {co_fg}. have charFpX: p \in [char {poly 'F_p}]. by rewrite (rmorph_char (polyC_rmorphism _)) ?char_Fp. diff --git a/mathcomp/field/falgebra.v b/mathcomp/field/falgebra.v index bdff38a..db235fe 100644 --- a/mathcomp/field/falgebra.v +++ b/mathcomp/field/falgebra.v @@ -1173,11 +1173,11 @@ by rewrite -aimgM limgS // [rhs in (_ <= rhs)%VS]agenvEl addvSr. Qed. Lemma aimg_adjoin (f : ahom aT rT) U x : (f @: <<U; x>> = <<f @: U; f x>>)%VS. -Proof. by rewrite aimg_agen limg_add limg_line. Qed. +Proof. by rewrite aimg_agen limgD limg_line. Qed. Lemma aimg_adjoin_seq (f : ahom aT rT) U xs : (f @: <<U & xs>> = <<f @: U & map f xs>>)%VS. -Proof. by rewrite aimg_agen limg_add limg_span. Qed. +Proof. by rewrite aimg_agen limgD limg_span. Qed. Fact ker_sub_ahom_is_aspace (f g : ahom aT rT) : is_aspace (lker (ahval f - ahval g)). diff --git a/mathcomp/field/fieldext.v b/mathcomp/field/fieldext.v index df7ef5a..d99b69b 100644 --- a/mathcomp/field/fieldext.v +++ b/mathcomp/field/fieldext.v @@ -1290,8 +1290,8 @@ Qed. Fact mulfx_addl : left_distributive subfext_mul subfext_add. Proof. -elim/quotW=> x; elim/quotW=> y; elim/quotW=> w; rewrite !piE /subfx_mul_rep. -by rewrite linearD /= mulrDl modp_add linearD. +elim/quotW=> x; elim/quotW=> y; elim/quotW=> w. +by rewrite !piE /subfx_mul_rep linearD /= mulrDl modpD linearD. Qed. Fact nonzero1fx : subfext1 != subfext0. @@ -1378,7 +1378,7 @@ Definition subfx_root := subfx_eval 'X. Lemma subfx_eval_is_rmorphism : rmorphism subfx_eval. Proof. do 2?split=> [x y|] /=; apply/eqP; rewrite piE. -- by rewrite -linearB modp_add modNp. +- by rewrite -linearB modpD modNp. - by rewrite /subfx_mul_rep !poly_rV_modp_K !(modp_mul, mulrC _ y). by rewrite modp_small // size_poly1 -subn_gt0 subn1. Qed. @@ -1529,7 +1529,7 @@ suffices [L dimL [toPF [toL toPF_K toL_K]]]: elim/poly_ind: q => [|a q IHq]. by rewrite map_poly0 horner0 linear0 mod0p. rewrite rmorphD rmorphM /= map_polyX map_polyC hornerMXaddC linearD /=. - rewrite linearZ /= -(rmorph1 toL) toL_K -modp_scalel alg_polyC modp_add. + rewrite linearZ /= -(rmorph1 toL) toL_K -modpZl alg_polyC modpD. congr (_ + _); rewrite -toL_K rmorphM /= -/z; congr (toPF (_ * z)). by apply: (can_inj toPF_K); rewrite toL_K. pose toL q : vL := poly_rV (q %% p); pose toPF (x : vL) := rVpoly x. @@ -1547,13 +1547,13 @@ have mul1: left_id L1 mul. by move=> x; apply: toPinj; rewrite mulC !toL_K modp_mul mulr1 -toL_K toPF_K. have mulD: left_distributive mul +%R. move=> x y z; apply: toPinj; rewrite /toPF raddfD /= -!/(toPF _). - by rewrite !toL_K /toPF raddfD mulrDl modp_add. + by rewrite !toL_K /toPF raddfD mulrDl modpD. have nzL1: L1 != 0 by rewrite -(inj_eq toPinj) L1K /toPF raddf0 oner_eq0. pose mulM := ComRingMixin mulA mulC mul1 mulD nzL1. pose rL := ComRingType (RingType vL mulM) mulC. have mulZl: GRing.Lalgebra.axiom mul. - move=> a x y; apply: toPinj; rewrite toL_K /toPF !linearZ /= -!/(toPF _). - by rewrite toL_K -scalerAl modp_scalel. + move=> a x y; apply: toPinj. + by rewrite toL_K /toPF !linearZ /= -!/(toPF _) toL_K -scalerAl modpZl. have mulZr: GRing.Algebra.axiom (LalgType F rL mulZl). by move=> a x y; rewrite !(mulrC x) scalerAl. pose aL := AlgType F _ mulZr; pose urL := FalgUnitRingType aL. @@ -1567,7 +1567,7 @@ have unitE: GRing.Field.mixin_of urL. rewrite dvdp_gcdl -ltnNge /= => /eqp_size->. by rewrite (polySpred nz_p) ltnS size_poly. suffices: x * toL u.2 = 1 by exists (toL u.2); rewrite mulrC. - apply: toPinj; rewrite !toL_K -upq1 modp_mul modp_add mulrC. + apply: toPinj; rewrite !toL_K -upq1 modp_mul modpD mulrC. by rewrite modp_mull add0r. pose ucrL := [comUnitRingType of ComRingType urL mulC]. have mul0 := GRing.Field.IdomainMixin unitE. @@ -1575,8 +1575,7 @@ pose fL := FieldType (IdomainType ucrL mul0) unitE. exists [fieldExtType F of faL for fL]; first by rewrite dimvf; apply: mul1n. exists [linear of toPF as rVpoly]. suffices toLM: lrmorphism (toL : {poly F} -> aL) by exists (LRMorphism toLM). -have toLlin: linear toL. - by move=> a q1 q2; rewrite -linearP -modp_scalel -modp_add. +have toLlin: linear toL by move=> a q1 q2; rewrite -linearP -modpZl -modpD. do ?split; try exact: toLlin; move=> q r /=. by apply: toPinj; rewrite !toL_K modp_mul -!(mulrC r) modp_mul. Qed. @@ -1607,13 +1606,13 @@ have mul1: left_id L1 mul. by rewrite size_poly. have mulD: left_distributive mul +%R. move=> x y z; apply: canLR rVpolyK _. - by rewrite !raddfD mulrDl /= !toL_K /toL modp_add. + by rewrite !raddfD mulrDl /= !toL_K /toL modpD. have nzL1: L1 != 0 by rewrite -(can_eq rVpolyK) L1K raddf0 oner_eq0. pose mulM := ComRingMixin mulA mulC mul1 mulD nzL1. pose rL := ComRingType (RingType vL mulM) mulC. have mulZl: GRing.Lalgebra.axiom mul. - move=> a x y; apply: canRL rVpolyK _; rewrite !linearZ /= toL_K. - by rewrite -scalerAl modp_scalel. + move=> a x y; apply: canRL rVpolyK _. + by rewrite !linearZ /= toL_K -scalerAl modpZl. have mulZr: @GRing.Algebra.axiom _ (LalgType F rL mulZl). by move=> a x y; rewrite !(mulrC x) scalerAl. pose aL := AlgType F _ mulZr; pose urL := FalgUnitRingType aL. @@ -1638,7 +1637,7 @@ have q_z q: rVpoly (map_poly iota q).[z] = q %% p. elim/poly_ind: q => [|a q IHq]. by rewrite map_poly0 horner0 linear0 mod0p. rewrite rmorphD rmorphM /= map_polyX map_polyC hornerMXaddC linearD /=. - rewrite linearZ /= L1K alg_polyC modp_add; congr (_ + _); last first. + rewrite linearZ /= L1K alg_polyC modpD; congr (_ + _); last first. by rewrite modp_small // size_polyC; case: (~~ _) => //; apply: ltnW. by rewrite !toL_K IHq mulrC modp_mul mulrC modp_mul. exists z; first by rewrite /root -(can_eq rVpolyK) q_z modpp linear0. diff --git a/mathcomp/field/separable.v b/mathcomp/field/separable.v index bc2eecb..e51a660 100644 --- a/mathcomp/field/separable.v +++ b/mathcomp/field/separable.v @@ -68,13 +68,13 @@ apply: (iffP idP) => [sep_p | [sq'p nz_der1p]]. split=> [u v | u u_dv_p]; last first. apply: contraTneq => u'0; rewrite -leqNgt -(eqnP sep_p). rewrite dvdp_leq -?size_poly_eq0 ?(eqnP sep_p) // dvdp_gcd u_dv_p. - have /dvdp_scaler <-: lead_coef u ^+ scalp p u != 0 by rewrite lcn_neq0. + have /dvdpZr <-: lead_coef u ^+ scalp p u != 0 by rewrite lcn_neq0. by rewrite -derivZ -Pdiv.Idomain.divpK //= derivM u'0 mulr0 addr0 dvdp_mull. rewrite Pdiv.Idomain.dvdp_eq mulrCA mulrA; set c := _ ^+ _ => /eqP Dcp. have nz_c: c != 0 by rewrite lcn_neq0. - move: sep_p; rewrite coprimep_sym -[separable _](coprimep_scalel _ _ nz_c). - rewrite -(coprimep_scaler _ _ nz_c) -derivZ Dcp derivM coprimep_mull. - by rewrite coprimep_addl_mul !coprimep_mulr -andbA => /and4P[]. + move: sep_p; rewrite coprimep_sym -[separable _](coprimepZl _ _ nz_c). + rewrite -(coprimepZr _ _ nz_c) -derivZ Dcp derivM coprimepMl. + by rewrite coprimep_addl_mul !coprimepMr -andbA => /and4P[]. rewrite /separable coprimep_def eqn_leq size_poly_gt0; set g := gcdp _ _. have nz_g: g != 0. rewrite -dvd0p dvdp_gcd -(mulr0 0); apply/nandP; left. @@ -82,9 +82,9 @@ have nz_g: g != 0. have [g_p]: g %| p /\ g %| p^`() by rewrite dvdp_gcdr ?dvdp_gcdl. pose c := lead_coef g ^+ scalp p g; have nz_c: c != 0 by rewrite lcn_neq0. have Dcp: c *: p = p %/ g * g by rewrite Pdiv.Idomain.divpK. -rewrite nz_g andbT leqNgt -(dvdp_scaler _ _ nz_c) -derivZ Dcp derivM. +rewrite nz_g andbT leqNgt -(dvdpZr _ _ nz_c) -derivZ Dcp derivM. rewrite dvdp_addr; last by rewrite dvdp_mull. -rewrite Gauss_dvdpr; last by rewrite sq'p // mulrC -Dcp dvdp_scalel. +rewrite Gauss_dvdpr; last by rewrite sq'p // mulrC -Dcp dvdpZl. by apply: contraL => /nz_der1p nz_g'; rewrite gtNdvdp ?nz_g' ?lt_size_deriv. Qed. @@ -114,8 +114,8 @@ Proof. apply/idP/and3P => [sep_pq | [sep_p seq_q co_pq]]. rewrite !(dvdp_separable _ sep_pq) ?dvdp_mulIr ?dvdp_mulIl //. by rewrite (separable_coprime sep_pq). -rewrite /separable derivM coprimep_mull {1}addrC mulrC !coprimep_addl_mul. -by rewrite !coprimep_mulr (coprimep_sym q p) co_pq !andbT; apply/andP. +rewrite /separable derivM coprimepMl {1}addrC mulrC !coprimep_addl_mul. +by rewrite !coprimepMr (coprimep_sym q p) co_pq !andbT; apply/andP. Qed. Lemma eqp_separable p q : p %= q -> separable p = separable q. @@ -145,10 +145,10 @@ split=> [|u u_pg u_gt1]; last first. apply/eqP=> u'0 /=; have [k /negP[]] := max_dvd_u u u_gt1. elim: k => [|k IHk]; first by rewrite dvd1p. suffices: u ^+ k.+1 %| (p %/ g) * g. - by rewrite Pdiv.Idomain.divpK ?dvdp_gcdl // dvdp_scaler ?lcn_neq0. + by rewrite Pdiv.Idomain.divpK ?dvdp_gcdl // dvdpZr ?lcn_neq0. rewrite exprS dvdp_mul // dvdp_gcd IHk //=. suffices: u ^+ k %| (p %/ u ^+ k * u ^+ k)^`(). - by rewrite Pdiv.Idomain.divpK // derivZ dvdp_scaler ?lcn_neq0. + by rewrite Pdiv.Idomain.divpK // derivZ dvdpZr ?lcn_neq0. by rewrite !derivCE u'0 mul0r mul0rn mulr0 addr0 dvdp_mull. have pg_dv_p: p %/ g %| p by rewrite divp_dvd ?dvdp_gcdl. apply/poly_square_freeP=> u; rewrite neq_ltn ltnS leqn0 size_poly_eq0. @@ -157,11 +157,11 @@ case/predU1P=> [-> | /max_dvd_u[k]]. apply: contra => u2_dv_pg; case: k; [by rewrite dvd1p | elim=> [|n IHn]]. exact: dvdp_trans (dvdp_mulr _ _) (dvdp_trans u2_dv_pg pg_dv_p). suff: u ^+ n.+2 %| (p %/ g) * g. - by rewrite Pdiv.Idomain.divpK ?dvdp_gcdl // dvdp_scaler ?lcn_neq0. + by rewrite Pdiv.Idomain.divpK ?dvdp_gcdl // dvdpZr ?lcn_neq0. rewrite -add2n exprD dvdp_mul // dvdp_gcd. rewrite (dvdp_trans _ IHn) ?exprS ?dvdp_mull //=. suff: u ^+ n %| ((p %/ u ^+ n.+1) * u ^+ n.+1)^`(). - by rewrite Pdiv.Idomain.divpK // derivZ dvdp_scaler ?lcn_neq0. + by rewrite Pdiv.Idomain.divpK // derivZ dvdpZr ?lcn_neq0. by rewrite !derivCE dvdp_add // -1?mulr_natl ?exprS !dvdp_mull. Qed. @@ -260,7 +260,7 @@ without loss{nz_q} sep_q: q qy_0 / separable_poly q. rewrite Dq rmorphM /= gcdp_map -(eqp_dvdr _ (gcdp_mul2l _ _ _)) -deriv_map Dr. rewrite dvdp_gcd derivM deriv_exp derivXsubC mul1r !mulrA dvdp_mulIr /=. rewrite mulrDr mulrA dvdp_addr ?dvdp_mulIr // exprS -scaler_nat -!scalerAr. - rewrite dvdp_scaler -?(rmorph_nat iota) ?fmorph_eq0 ?charF0 //. + rewrite dvdpZr -?(rmorph_nat iota) ?fmorph_eq0 ?charF0 //. rewrite mulrA dvdp_mul2r ?expf_neq0 ?polyXsubC_eq0 //. by rewrite Gauss_dvdpl ?dvdp_XsubCl // coprimep_sym coprimep_XsubC. have [r nz_r PETxy] := large_field_PET qy_0 sep_q. @@ -585,7 +585,7 @@ elim: n => // n IHn in x @d *; rewrite ltnS => le_d_n. have [[p charLp]|] := altP (separablePn K x); last by rewrite negbK; exists 1%N. case=> g Kg defKx; have p_pr := charf_prime charLp. suffices /IHn[m /andP[charLm sepKxpm]]: adjoin_degree K (x ^+ p) < n. - by exists (p * m)%N; rewrite pnat_mul pnatE // charLp charLm exprM. + by exists (p * m)%N; rewrite pnatM pnatE // charLp charLm exprM. apply: leq_trans le_d_n; rewrite -ltnS -!size_minPoly. have nzKx: minPoly K x != 0 by rewrite monic_neq0 ?monic_minPoly. have nzg: g != 0 by apply: contra_eqN defKx => /eqP->; rewrite comp_poly0. @@ -844,7 +844,7 @@ Lemma inseparable_add K x y : Proof. have insepP := purely_inseparable_elementP. move=> /insepP[n charLn Kxn] /insepP[m charLm Kym]; apply/insepP. -have charLnm: [char L].-nat (n * m)%N by rewrite pnat_mul charLn. +have charLnm: [char L].-nat (n * m)%N by rewrite pnatM charLn. by exists (n * m)%N; rewrite ?exprDn_char // {2}mulnC !exprM memvD // rpredX. Qed. @@ -944,7 +944,7 @@ by apply/FadjoinP/andP; rewrite sKE separable_generator_mem. Qed. Lemma separable_refl K : separable K K. -Proof. by apply/separableP; apply: base_separable. Qed. +Proof. exact/separableP/base_separable. Qed. Lemma separable_trans M K E : separable K M -> separable M E -> separable K E. Proof. @@ -986,7 +986,7 @@ Proof. have insepP := purely_inseparableP => /insepP insepK_M /insepP insepM_E. have insepPe := purely_inseparable_elementP. apply/insepP=> x /insepM_E/insepPe[n charLn /insepK_M/insepPe[m charLm Kxnm]]. -by apply/insepPe; exists (n * m)%N; rewrite ?exprM // pnat_mul charLn charLm. +by apply/insepPe; exists (n * m)%N; rewrite ?exprM // pnatM charLn charLm. Qed. End Separable. |