diff options
Diffstat (limited to 'mathcomp/field')
| -rw-r--r-- | mathcomp/field/algebraics_fundamentals.v | 2 | ||||
| -rw-r--r-- | mathcomp/field/algnum.v | 2 | ||||
| -rw-r--r-- | mathcomp/field/closed_field.v | 9 | ||||
| -rw-r--r-- | mathcomp/field/cyclotomic.v | 12 | ||||
| -rw-r--r-- | mathcomp/field/fieldext.v | 4 | ||||
| -rw-r--r-- | mathcomp/field/galois.v | 13 | ||||
| -rw-r--r-- | mathcomp/field/separable.v | 18 |
7 files changed, 31 insertions, 29 deletions
diff --git a/mathcomp/field/algebraics_fundamentals.v b/mathcomp/field/algebraics_fundamentals.v index 2d576c4..18fa55a 100644 --- a/mathcomp/field/algebraics_fundamentals.v +++ b/mathcomp/field/algebraics_fundamentals.v @@ -648,7 +648,7 @@ have /all_sig[n_ FTA] z: {n | z \in sQ (z_ n)}. have [p]: exists p, [&& p \is monic, root p z & p \is a polyOver (sQ (z_ n))]. have [p mon_p pz0] := algC z; exists (p ^ QtoC). by rewrite map_monic mon_p pz0 -(pQof (z_ n)); apply/polyOver_poly. - elim: {p}_.+1 {-2}p n (ltnSn (size p)) => // d IHd p n lepd pz0. + have [d lepd] := ubnP (size p); elim: d => // d IHd in p n lepd * => pz0. have [t [t_C t_z gal_t]]: exists t, [/\ z_ n \in sQ t, z \in sQ t & is_Gal t]. have [y /and3P[y_C y_z _]] := PET [:: z_ n; z]. by have [t /(sQtrans y)t_y] := galQ y; exists t; rewrite !t_y. diff --git a/mathcomp/field/algnum.v b/mathcomp/field/algnum.v index f494a09..c191a0e 100644 --- a/mathcomp/field/algnum.v +++ b/mathcomp/field/algnum.v @@ -439,7 +439,7 @@ have nu_inj n y: nu (Sinj (ext n) y) = Sinj (ext n) (Saut (ext n) y). rewrite /nu; case: (mem_ext _ _ _); move: _.+1 => n1 y1 Dy /=. without loss /subnK Dn1: n n1 y y1 Dy / (n <= n1)%N. by move=> IH; case/orP: (leq_total n n1) => /IH => [/(_ y) | /(_ y1)]->. - elim: {n}(_ - n)%N {-1}n => [|k IHk] n in Dn1 y Dy *. + move: (n1 - n)%N => k in Dn1; elim: k => [|k IHk] in n Dn1 y Dy *. by move: y1 Dy; rewrite -Dn1 => y1 /fmorph_inj ->. rewrite addSnnS in Dn1; move/IHk: Dn1 => /=. case: (unpickle _) => [z|] /=; last exact. diff --git a/mathcomp/field/closed_field.v b/mathcomp/field/closed_field.v index b55a48e..a6f7514 100644 --- a/mathcomp/field/closed_field.v +++ b/mathcomp/field/closed_field.v @@ -878,10 +878,11 @@ have Kclosed: GRing.ClosedField.axiom Kfield. apply/eqP; rewrite EtoKeq0 (eq_map_poly (toEleS _ _ _ _)) map_poly_comp Dpj. rewrite -rootE -[pj]minXpE ?ext1root // -Dpj size_map_poly. by rewrite size_addl ?size_polyXn ltnS ?size_opp ?size_poly. - rewrite {w}/pj; elim: {-9}j lemj => // k IHk lemSk. - move: lemSk (lemSk); rewrite {1}leq_eqVlt ltnS => /predU1P[<- | lemk] lemSk. - rewrite {k IHk lemSk}(eq_map_poly (toEeq m _)) map_poly_id //= /incEp. - by rewrite codeK eqxx pickleK. + rewrite {w}/pj; set j0 := (j in tagged (E_ _) j). + elim: {+}j lemj => // k IHk lemSk; rewrite {}/j0 in IHk *. + have:= lemSk; rewrite leq_eqVlt ltnS => /predU1P[Dm | lemk]. + rewrite -{}Dm in lemSk *; rewrite {k IHk lemSk}(eq_map_poly (toEeq m _)). + by rewrite map_poly_id //= /incEp codeK eqxx pickleK. rewrite (eq_map_poly (toEleS _ _ _ _)) map_poly_comp {}IHk //= /incEp codeK. by rewrite -if_neg neq_ltn lemk. suffices{Kclosed} algF_K: {FtoK : {rmorphism F -> Kfield} | integralRange FtoK}. diff --git a/mathcomp/field/cyclotomic.v b/mathcomp/field/cyclotomic.v index dcb4a5b..d80a909 100644 --- a/mathcomp/field/cyclotomic.v +++ b/mathcomp/field/cyclotomic.v @@ -149,7 +149,7 @@ Qed. Lemma Cintr_Cyclotomic n z : n.-primitive_root z -> pZtoC 'Phi_n = cyclotomic z n. Proof. -elim: {n}_.+1 {-2}n z (ltnSn n) => // m IHm n z0 le_mn prim_z0. +elim/ltn_ind: n z => n IHn z0 prim_z0. rewrite /'Phi_n; case: (C_prim_root_exists _) => z /=. have n_gt0 := prim_order_gt0 prim_z0; rewrite prednK // => prim_z. have [uDn _ inDn] := divisors_correct n_gt0. @@ -159,8 +159,7 @@ have defXn1: cyclotomic z n * pZtoC q = 'X^n - 1. rewrite (prod_cyclotomic prim_z) (big_rem n) ?inDn //=. rewrite divnn n_gt0 rmorph_prod /=; congr (_ * _). apply: eq_big_seq => d; rewrite mem_rem_uniq ?inE //= inDn => /andP[n'd ddvn]. - rewrite -IHm ?dvdn_prim_root // -ltnS (leq_ltn_trans _ le_mn) //. - by rewrite ltn_neqAle n'd dvdn_leq. + by rewrite -IHn ?dvdn_prim_root // ltn_neqAle n'd dvdn_leq. have mapXn1 (R1 R2 : ringType) (f : {rmorphism R1 -> R2}): map_poly f ('X^n - 1) = 'X^n - 1. - by rewrite rmorphB /= rmorph1 map_polyXn. @@ -263,8 +262,7 @@ have co_fg (R : idomainType): n%:R != 0 :> R -> @coprimep R (intrp f) (intrp g). suffices fzk0: root (pZtoC f) zk. have [] // := negP (coprimep_root (co_fg _ _) fzk0). by rewrite pnatr_eq0 -lt0n. -move: gzk0 cokn; rewrite {zk}Dzk; elim: {k}_.+1 {-2}k (ltnSn k) => // m IHm k. -rewrite ltnS => lekm gzk0 cokn. +move: gzk0 cokn; rewrite {zk}Dzk; elim/ltn_ind: k => k IHk gzk0 cokn. have [|k_gt1] := leqP k 1; last have [p p_pr /dvdnP[k1 Dk]] := pdivP k_gt1. rewrite -[leq k 1](mem_iota 0 2) !inE => /pred2P[k0 | ->]; last first. by rewrite -Df dv_pf. @@ -287,8 +285,8 @@ suffices: coprimep (pZtoC f) (pZtoC (g \Po 'X^p)). rewrite -exprM -Dk [_ == 0]gzk0 implybF => /negP[]. have: root pz (z ^+ k1). by rewrite root_cyclotomic // prim_root_exp_coprime. - rewrite -Dpz -Dfg rmorphM rootM => /orP[] //= /IHm-> //. - rewrite (leq_trans _ lekm) // -[k1]muln1 Dk ltn_pmul2l ?prime_gt1 //. + rewrite -Dpz -Dfg rmorphM rootM => /orP[] //= /IHk-> //. + rewrite -[k1]muln1 Dk ltn_pmul2l ?prime_gt1 //. by have:= ltnW k_gt1; rewrite Dk muln_gt0 => /andP[]. suffices: coprimep f (g \Po 'X^p). case/Bezout_coprimepP=> [[u v]]; rewrite -size_poly_eq1. diff --git a/mathcomp/field/fieldext.v b/mathcomp/field/fieldext.v index 64239f3..86d3d39 100644 --- a/mathcomp/field/fieldext.v +++ b/mathcomp/field/fieldext.v @@ -555,8 +555,8 @@ Qed. Lemma Fadjoin_sum_direct : directv sumKx. Proof. -rewrite directvE /=; case Dn: {-2}n (leqnn n) => // [m] {Dn}. -elim: m => [|m IHm] ltm1n; rewrite ?big_ord1 // !(big_ord_recr m.+1) /=. +rewrite directvE /=; case: (ubnPgeq n) (isT : n > 0) => -[//|m] ltmn _. +elim: m ltmn => [|m IHm] ltm1n; rewrite ?big_ord1 // !(big_ord_recr m.+1) /=. do [move/(_ (ltnW ltm1n))/eqP; set S := (\sum_i _)%VS] in IHm *. rewrite -IHm dimv_add_leqif; apply/subvP=> z; rewrite memv_cap => /andP[Sz]. case/memv_cosetP=> y Ky Dz; rewrite memv0 Dz mulf_eq0 expf_eq0 /=. diff --git a/mathcomp/field/galois.v b/mathcomp/field/galois.v index 7937a24..4aaef57 100644 --- a/mathcomp/field/galois.v +++ b/mathcomp/field/galois.v @@ -561,7 +561,7 @@ have [[p F0p splitLp] [autL DautL]] := (splittingFieldP, enum_AEnd). suffices{K} autL_px q: q != 0 -> q %| q1 -> size q > 1 -> has (fx_root q) autL. set q := minPoly K x; have: q \is monic := monic_minPoly K x. have: q %| q1 by rewrite minPolyS // sub1v. - elim: {q}_.+1 {-2}q (ltnSn (size q)) => // d IHd q leqd q_dv_q1 mon_q. + have [d] := ubnP (size q); elim: d q => // d IHd q leqd q_dv_q1 mon_q. have nz_q: q != 0 := monic_neq0 mon_q. have [|q_gt1|q_1] := ltngtP (size q) 1; last first; last by rewrite polySpred. by exists nil; rewrite big_nil -eqp_monic ?monic1 // -size_poly_eq1 q_1. @@ -571,7 +571,7 @@ suffices{K} autL_px q: q != 0 -> q %| q1 -> size q > 1 -> has (fx_root q) autL. have q2_dv_q1: q2 %| q1 by rewrite (dvdp_trans _ q_dv_q1) // Dq dvdp_mulr. rewrite Dq; have [r /eqP->] := IHd q2 leqd q2_dv_q1 mon_q2. by exists (f x :: r); rewrite big_cons mulrC. -elim: {q}_.+1 {-2}q (ltnSn (size q)) => // d IHd q leqd nz_q q_dv_q1 q_gt1. +have [d] := ubnP (size q); elim: d q => // d IHd q leqd nz_q q_dv_q1 q_gt1. without loss{d leqd IHd nz_q q_gt1} irr_q: q q_dv_q1 / irreducible_poly q. move=> IHq; apply: wlog_neg => not_autLx_q; apply: IHq => //. split=> // q2 q2_neq1 q2_dv_q; rewrite -dvdp_size_eqp // eqn_leq dvdp_leq //=. @@ -645,9 +645,10 @@ have [f homLf fxz]: exists2 f : 'End(Lz), kHom 1 imL f & f (inLz x) = z. pose f1 := (inLz^-1 \o f \o inLz)%VF; have /kHomP[fM fFid] := homLf. have Df1 u: inLz (f1 u) = f (inLz u). rewrite !comp_lfunE limg_lfunVK //= -[limg _]/(asval imL). - have [r def_pz defLz] := splitLpz. - have []: all (mem r) r /\ inLz u \in imL by split; first apply/allP. - rewrite -{1}defLz; elim/last_ind: {-1}r {u}(inLz u) => [|r1 y IHr1] u. + have [r def_pz defLz] := splitLpz; set r1 := r. + have: inLz u \in <<1 & r1>>%VS by rewrite defLz. + have: all (mem r) r1 by apply/allP. + elim/last_ind: r1 {u}(inLz u) => [|r1 y IHr1] u. by rewrite Fadjoin_nil => _ Fu; rewrite fFid // (subvP (sub1v _)). rewrite all_rcons adjoin_rcons => /andP[rr1 ry] /Fadjoin_polyP[pu r1pu ->]. rewrite (kHom_horner homLf) -defLz; last exact: seqv_sub_adjoin; last first. @@ -1353,7 +1354,7 @@ Lemma gal_independent_contra E (P : pred (gal_of E)) (c_ : gal_of E -> L) x : P x -> c_ x != 0 -> exists2 a, a \in E & \sum_(y | P y) c_ y * y a != 0. Proof. -elim: {P}_.+1 c_ x {-2}P (ltnSn #|P|) => // n IHn c_ x P lePn Px nz_cx. +have [n] := ubnP #|P|; elim: n c_ x P => // n IHn c_ x P lePn Px nz_cx. 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. diff --git a/mathcomp/field/separable.v b/mathcomp/field/separable.v index a482632..bc2eecb 100644 --- a/mathcomp/field/separable.v +++ b/mathcomp/field/separable.v @@ -482,9 +482,9 @@ Lemma extendDerivation_horner p : extendDerivation K p.[x] = (map_poly D p).[x] + p^`().[x] * Dx K. Proof. move=> Kp sepKx; have:= separable_root_der; rewrite {}sepKx /= => nz_pKx'x. -rewrite {-1}(divp_eq p (minPoly K x)) lfunE /= Fadjoin_poly_mod // raddfD /=. -rewrite {1}(Derivation_mul_poly derD) ?divp_polyOver ?minPolyOver //. -rewrite derivD derivM !{1}hornerD !{1}hornerM minPolyxx !{1}mulr0 !{1}add0r. +rewrite [in RHS](divp_eq p (minPoly K x)) lfunE /= Fadjoin_poly_mod ?raddfD //=. +rewrite (Derivation_mul_poly derD) ?divp_polyOver ?minPolyOver //. +rewrite derivM !{1}hornerD !{1}hornerM minPolyxx !{1}mulr0 !{1}add0r. rewrite mulrDl addrA [_ + (_ * _ * _)]addrC {2}/Dx -mulrA -/Dx. by rewrite [_ / _]mulrC (mulVKf nz_pKx'x) mulrN addKr. Qed. @@ -528,12 +528,14 @@ have DK_0: (K <= lker D)%VS. apply/subvP=> v Kv; rewrite memv_ker lfunE /= Fadjoin_polyC //. by rewrite derivC horner0. have Dder: Derivation <<K; x>> D. - apply/allP=> u /vbasis_mem Kx_u; apply/allP=> v /vbasis_mem Kx_v. - rewrite !lfunE /= -{-2}(Fadjoin_poly_eq Kx_u) -{-3}(Fadjoin_poly_eq Kx_v). + apply/allP=> u /vbasis_mem Kx_u; apply/allP=> v /vbasis_mem Kx_v; apply/eqP. + rewrite !lfunE /=; set Px := Fadjoin_poly K x. + set Px_u := Px u; rewrite -(Fadjoin_poly_eq Kx_u) -/Px -/Px_u. + set Px_v := Px v; rewrite -(Fadjoin_poly_eq Kx_v) -/Px -/Px_v. rewrite -!hornerM -hornerD -derivM. - rewrite Fadjoin_poly_mod ?rpredM ?Fadjoin_polyOver //. - rewrite {2}(divp_eq (_ * _) (minPoly K x)) derivD derivM pKx'_0 mulr0 addr0. - by rewrite hornerD hornerM minPolyxx mulr0 add0r. + rewrite /Px Fadjoin_poly_mod ?rpredM ?Fadjoin_polyOver //. + rewrite [in RHS](divp_eq (Px_u * Px_v) (minPoly K x)) derivD derivM. + by rewrite pKx'_0 mulr0 addr0 hornerD hornerM minPolyxx mulr0 add0r. have{Dder DK_0}: x \in lker D by apply: subvP Kx_x; apply: derKx_0. apply: contraLR => K'x; rewrite memv_ker lfunE /= Fadjoin_polyX //. by rewrite derivX hornerC oner_eq0. |