diff options
Diffstat (limited to 'mathcomp/field')
| -rw-r--r-- | mathcomp/field/Make | 2 | ||||
| -rw-r--r-- | mathcomp/field/algC.v | 4 | ||||
| -rw-r--r-- | mathcomp/field/algebraics_fundamentals.v | 8 | ||||
| -rw-r--r-- | mathcomp/field/algnum.v | 4 | ||||
| -rw-r--r-- | mathcomp/field/closed_field.v | 4 | ||||
| -rw-r--r-- | mathcomp/field/cyclotomic.v | 4 | ||||
| -rw-r--r-- | mathcomp/field/fieldext.v | 8 | ||||
| -rw-r--r-- | mathcomp/field/finfield.v | 4 | ||||
| -rw-r--r-- | mathcomp/field/galois.v | 8 | ||||
| -rw-r--r-- | mathcomp/field/separable.v | 6 |
10 files changed, 26 insertions, 26 deletions
diff --git a/mathcomp/field/Make b/mathcomp/field/Make index c906bd9..93795e9 100644 --- a/mathcomp/field/Make +++ b/mathcomp/field/Make @@ -15,6 +15,6 @@ separable.v -arg -w -arg -projection-no-head-constant -arg -w -arg -redundant-canonical-projection -arg -w -arg -notation-overridden --arg -w -arg -duplicate-clear +-arg -w -arg +duplicate-clear -arg -w -arg -ambiguous-paths -arg -w -arg +undeclared-scope
\ No newline at end of file diff --git a/mathcomp/field/algC.v b/mathcomp/field/algC.v index 815bfba..68e1ba7 100644 --- a/mathcomp/field/algC.v +++ b/mathcomp/field/algC.v @@ -71,14 +71,14 @@ have nz2: 2%:R != 0 :> L. apply/eqP=> char2; apply: conj_nt => e; apply/eqP/idPn=> eJ. have opp_id x: - x = x :> L. by apply/esym/eqP; rewrite -addr_eq0 -mulr2n -mulr_natl char2 mul0r. - have{char2} char2: 2 \in [char L] by apply/eqP. + have{} char2: 2 \in [char L] by apply/eqP. without loss{eJ} eJ: e / conj e = e + 1. move/(_ (e / (e + conj e))); apply. rewrite fmorph_div rmorphD conjK -{1}[conj e](addNKr e) mulrDl. by rewrite opp_id (addrC e) divff // addr_eq0 opp_id. pose a := e * conj e; have aJ: conj a = a by rewrite rmorphM conjK mulrC. have [w Dw] := @solve_monicpoly _ 2 (nth 0 [:: e * a; - 1]) isT. - have{Dw} Dw: w ^+ 2 + w = e * a. + have{} Dw: w ^+ 2 + w = e * a. by rewrite Dw !big_ord_recl big_ord0 /= mulr1 mulN1r addr0 subrK. pose b := w + conj w; have bJ: conj b = b by rewrite rmorphD conjK addrC. have Db2: b ^+ 2 + b = a. diff --git a/mathcomp/field/algebraics_fundamentals.v b/mathcomp/field/algebraics_fundamentals.v index a950ecc..c956047 100644 --- a/mathcomp/field/algebraics_fundamentals.v +++ b/mathcomp/field/algebraics_fundamentals.v @@ -239,7 +239,7 @@ without loss{nCq} qx0: q mon_q q_dv_p / root (q ^ FtoL) x. rewrite -(subnn (size q1)) {1}IHq1 ?Dp ?dvdp_mulr // polySpred ?monic_neq0 //. by rewrite eqSS size_monicM ?monic_neq0 // -!subn1 subnAC addKn. have /dvdp_prod_XsubC[m Dq]: q ^ FtoL %| p_ I by rewrite DpI dvdp_map. -pose B := [set j in mask m (enum I)]; have{Dq} Dq: q ^ FtoL = p_ B. +pose B := [set j in mask m (enum I)]; have{} Dq: q ^ FtoL = p_ B. apply/eqP; rewrite -eqp_monic ?monic_map ?monic_prod_XsubC //. congr (_ %= _): Dq; apply: perm_big => //. by rewrite uniq_perm ?mask_uniq ?enum_uniq // => j; rewrite mem_enum inE. @@ -372,7 +372,7 @@ pose root_in (xR : realC) p := exists2 w, w \in sQ (tag xR) & root p w. pose extendsR (xR yR : realC) := tag xR \in sQ (tag yR). have add_Rroot xR p c: {yR | extendsR xR yR & has_Rroot xR p c -> root_in yR p}. rewrite {}/extendsR; case: (has_Rroot xR p c) / and4P; last by exists xR. - case: xR => x [R QxR] /= [/inQpK <-]; move: (p ^ _) => {p}p mon_p /inQ_K<- Dc. + case: xR => x [R QxR] /= [/inQpK <-]; move: (p ^ _) => {}p mon_p /inQ_K<- Dc. have{c Dc} p0_le0: (p ^ QxR).[0] <= 0. rewrite horner_coef0 coef_map -[p`_0]ofQ_K -coef_map -horner_coef0 (eqP Dc). by rewrite -rmorphX -rmorphN ofQ_K /= rmorphN rmorphX oppr_le0 sqr_ge0. @@ -417,7 +417,7 @@ have add_Rroot xR p c: {yR | extendsR xR yR & has_Rroot xR p c -> root_in yR p}. exists u => {s s_y}//; set y := ofQ z (t_ u); set p1 := minPoly Qx u in Dp. have /QtoQ[Qyz QyzE]: y \in sQ z := sQof z (t_ u). pose q1_ v := Fadjoin_poly Qx u (Qyz v). - have{QyzE} QyzE v: Qyz v = (q1_ v).[u]. + have{} QyzE v: Qyz v = (q1_ v).[u]. by rewrite Fadjoin_poly_eq // -Dt -sQof2 QyzE sQof. have /all_sig2[q_ coqp Dq] v: {q | v != 0 -> coprimep p q & q ^ Qxz = q1_ v}. have /pQwx[q Dq]: q1_ v \is a polyOver Qx by apply: Fadjoin_polyOver. @@ -572,7 +572,7 @@ have add_Rroot xR p c: {yR | extendsR xR yR & has_Rroot xR p c -> root_in yR p}. have /(find_root ((d * e)^-1 *: r ^ QxR))[N ub_rp] := xab0. pose f := d * e * h2; apply/posP; exists (maxn N (maxn m n)), f => [|k]. by rewrite !mulr_gt0 ?invr_gt0 ?ltr0n. - rewrite !geq_max => /and3P[/ab_le/ub_rp{ub_rp}ub_rp le_mk le_nk]. + rewrite !geq_max => /and3P[/ab_le/ub_rp{}ub_rp le_mk le_nk]. rewrite -(ltr_add2r f) -mulr2n -mulr_natr divfK // /nlim /lim Dqvw. rewrite rmorphD hornerD /= -addrA -ltr_subl_addl ler_lt_add //. by rewrite rmorphM hornerM ler_pmul ?ltW ?v_gtd ?w_gte. diff --git a/mathcomp/field/algnum.v b/mathcomp/field/algnum.v index bed8e71..0b1e892 100644 --- a/mathcomp/field/algnum.v +++ b/mathcomp/field/algnum.v @@ -392,7 +392,7 @@ have ext1 mu0 x: {mu1 | exists y, x = Sinj mu1 y suffices in01M: lrmorphism in01 by exists (LRMorphism in01M). pose rwM := (=^~ Din01, SinjZ, rmorph1, rmorphB, rmorphM). by do 3?split; try move=> ? ?; apply: (fmorph_inj QrC); rewrite !rwM. - have {z zz Dz px Dx} Dx: exists xx, x = QrC xx. + have {z zz Dz px} Dx: exists xx, x = QrC xx. exists (map_poly (in_alg Qr) px).[zz]. by rewrite -horner_map Dz Sinj_poly Dx. pose lin01 := linfun in01; pose K := (lin01 @: fullv)%VS. @@ -637,7 +637,7 @@ Proof. have ZP_C c: (ZtoC c)%:P \is a polyOver Cint by rewrite raddfMz rpred_int. move=> mulS S_P x Sx; pose v := \row_(i < n) Y`_i. have [v0 | nz_v] := eqVneq v 0. - case/S_P: Sx => {x}x ->; rewrite big1 ?isAlgInt0 // => i _. + case/S_P: Sx => {}x ->; rewrite big1 ?isAlgInt0 // => i _. by have /rowP/(_ i) := v0; rewrite !mxE => ->; rewrite mul0rz. have sYS (i : 'I_n): x * Y`_i \in S. by rewrite rpredM //; apply/S_P/Cint_spanP/mem_Cint_span/memt_nth. diff --git a/mathcomp/field/closed_field.v b/mathcomp/field/closed_field.v index 266788c..24b764b 100644 --- a/mathcomp/field/closed_field.v +++ b/mathcomp/field/closed_field.v @@ -538,7 +538,7 @@ elim: t; do ?[ by move=> * //=; do ?case: (_ == _)]. - by move=> t irt /= n rt; rewrite rpoly_map_mul ?irt //. - move=> t irt s irs /=; case/andP=> rt rs. by apply: rmulpT; rewrite ?irt ?irs //. -- move=> t irt /= n rt; move: (irt rt)=> {rt} rt; elim: n => [|n ihn] //=. +- move=> t irt /= n rt; move: (irt rt) => {}rt; elim: n => [|n ihn] //=. exact: rmulpT. Qed. @@ -886,7 +886,7 @@ suffices{Kclosed} algF_K: {FtoK : {rmorphism F -> Kfield} | integralRange FtoK}. pose Kdec := DecFieldType Kfield (closed_field_QEMixin Kclosed). pose KclosedField := ClosedFieldType Kdec Kclosed. by exists [countClosedFieldType of CountType KclosedField cntK]. -exists (EtoKM 0%N) => /= z; have [i [{z}z ->]] := KtoE z. +exists (EtoKM 0%N) => /= z; have [i [{}z ->]] := KtoE z. suffices{z} /(_ z)[p mon_p]: integralRange (toE 0%N i isT). by rewrite -(fmorph_root (EtoKM i)) -map_poly_comp toEtoKp; exists p. rewrite /toE /E; clear - minXp_gt1 ext1root ext1gen. diff --git a/mathcomp/field/cyclotomic.v b/mathcomp/field/cyclotomic.v index 5359cce..a6ba3bc 100644 --- a/mathcomp/field/cyclotomic.v +++ b/mathcomp/field/cyclotomic.v @@ -234,7 +234,7 @@ without loss{nz_af} [mon_f mon_g]: af f g Df Dfg / f \is monic /\ g \is monic. - by rewrite rmorphMz -scalerMzr scalerMzl -mulrzA cfg1. - by rewrite mulrzAl mulrzAr -mulrzA cfg1. by rewrite !(intz, =^~ scaler_int) !monicE !lead_coefZ mulrC cfg1. -have{af Df} Df: pQtoC pf = pZtoC f. +have{af} Df: pQtoC pf = pZtoC f. have:= congr1 lead_coef Df. rewrite lead_coefZ lead_coef_map_inj //; last exact: intr_inj. rewrite !(monicP _) // mulr1 Df => <-; rewrite scale1r -map_poly_comp. @@ -289,7 +289,7 @@ suffices: coprimep (pZtoC f) (pZtoC (g \Po 'X^p)). suffices: coprimep f (g \Po 'X^p). case/Bezout_coprimepP=> [[u v]]; rewrite -size_poly_eq1. rewrite -(size_map_inj_poly (can_inj intCK)) // rmorphD !rmorphM /=. - rewrite size_poly_eq1 => {co_fg}co_fg; apply/Bezout_coprimepP. + rewrite size_poly_eq1 => {}co_fg; apply/Bezout_coprimepP. by exists (pZtoC u, pZtoC v). apply: contraLR co_fg => /coprimepPn[|d]; first exact: monic_neq0. rewrite andbC -size_poly_eq1 dvdp_gcd => /and3P[sz_d]. diff --git a/mathcomp/field/fieldext.v b/mathcomp/field/fieldext.v index d99b69b..9091dd8 100644 --- a/mathcomp/field/fieldext.v +++ b/mathcomp/field/fieldext.v @@ -680,7 +680,7 @@ rewrite rootM => pqx0 szpq. have [nzq nzp]: q != 0 /\ p != 0. by apply/norP; rewrite -mulf_eq0 -size_poly_eq0 szpq. without loss{pqx0} qx0: q p Kp Kq nzp nzq szpq / root q x. - move=> IH; case/orP: pqx0 => /IH{IH}IH; first exact: IH. + move=> IH; case/orP: pqx0 => /IH{}IH; first exact: IH. have{IH} /orP[]: (q %= p * q) || (q %= 1) by apply: IH => //; rewrite mulrC. by rewrite orbC -{1}[q]mul1r eqp_mul2r // eqp_sym => ->. by rewrite -{1}[p]mul1r eqp_sym eqp_mul2r // => ->. @@ -875,7 +875,7 @@ Implicit Types (V : {vspace L}) (E : {subfield L}). Lemma trivial_fieldOver : (1%VS : {vspace L_F}) =i F. Proof. -move=> x; apply/vlineP/idP=> [[{x}x ->] | Fx]. +move=> x; apply/vlineP/idP=> [[{}x ->] | Fx]. by rewrite fieldOver_scaleE mulr1 (valP x). by exists (vsproj F x); rewrite fieldOver_scaleE mulr1 vsprojK. Qed. @@ -912,7 +912,7 @@ suff: basis_of (vspaceOver M) b by apply: size_basis. apply/andP; split. rewrite eqEsubv; apply/andP; split; apply/span_subvP=> u. by rewrite mem_vspaceOver field_module_eq // => /Mb. - move/(@vbasis_mem _ _ _ M); rewrite -defM => /memv_sumP[{u}u Fu ->]. + move/(@vbasis_mem _ _ _ M); rewrite -defM => /memv_sumP[{}u Fu ->]. apply: memv_suml => i _; have /memv_cosetP[a Fa ->] := Fu i isT. by apply: (memvZ (Subvs Fa)); rewrite memv_span ?memt_nth. apply/freeP=> a /(directv_sum_independent dx_b) a_0 i. @@ -1109,7 +1109,7 @@ move=> v; rewrite -{1}(field_module_eq modM0) -(mem_vspaceOver M0) {}/V. move: (vspaceOver F1 M0) => M. apply/idP/idP=> [/coord_vbasis|/coord_span]->; apply/memv_suml=> i _. rewrite /(_ *: _) /= /fieldOver_scale; case: (coord _ i _) => /= x. - rewrite {1}[F1]unlock mem_baseVspace => /vlineP[{x}x ->]. + rewrite {1}[F1]unlock mem_baseVspace => /vlineP[{}x ->]. by rewrite -(@scalerAl F L) mul1r memvZ ?memv_span ?memt_nth. move: (coord _ i _) => x; rewrite -[_`_i]mul1r scalerAl -tnth_nth. have F1x: x%:A \in F1. diff --git a/mathcomp/field/finfield.v b/mathcomp/field/finfield.v index 492aed8..19684dc 100644 --- a/mathcomp/field/finfield.v +++ b/mathcomp/field/finfield.v @@ -405,7 +405,7 @@ have fZ: linear f. have /kAut_to_gal[alpha galLalpha Dalpha]: kAut 1 {:L} (linfun (Linear fZ)). rewrite kAutfE; apply/kHomP; split=> [x y _ _ | x /idfP]; rewrite !lfunE //=. exact: (rmorphM (RMorphism fM)). -have{Dalpha} Dalpha: alpha =1 f by move=> a; rewrite -Dalpha ?memvf ?lfunE. +have{} Dalpha: alpha =1 f by move=> a; rewrite -Dalpha ?memvf ?lfunE. suffices <-: fixedField [set alpha] = 1%AS. by rewrite gal_generated /generator; exists alpha. apply/vspaceP=> x; apply/fixedFieldP/idfP; rewrite ?memvf // => id_x. @@ -442,7 +442,7 @@ End FinGalois. Lemma Fermat's_little_theorem (L : fieldExtType F) (K : {subfield L}) a : (a \in K) = (a ^+ order K == a). Proof. -move: K a; wlog [{L}L -> K a]: L / exists galL : splittingFieldType F, L = galL. +move: K a; wlog [{}L -> K a]: L / exists galL : splittingFieldType F, L = galL. by pose galL := (FinSplittingFieldType F L) => /(_ galL); apply; exists galL. have /galois_fixedField fixLK := finField_galois (subvf K). have [alpha defGalLK Dalpha] := finField_galois_generator (subvf K). diff --git a/mathcomp/field/galois.v b/mathcomp/field/galois.v index 82c4819..f41ec06 100644 --- a/mathcomp/field/galois.v +++ b/mathcomp/field/galois.v @@ -158,7 +158,7 @@ Definition kHom_rmorphism K E f homKEf := Lemma kHom_horner K E f p x : kHom K E f -> p \is a polyOver E -> x \in E -> f p.[x] = (map_poly f p).[f x]. Proof. -move=> homKf /polyOver_subvs[{p}p -> Ex]; pose fRM := kHom_rmorphism homKf. +move=> homKf /polyOver_subvs[{}p -> Ex]; pose fRM := kHom_rmorphism homKf. by rewrite (horner_map _ _ (Subvs Ex)) -[f _](horner_map fRM) map_poly_comp. Qed. @@ -632,7 +632,7 @@ have [f homLf fxz]: exists2 f : 'End(Lz), kHom 1 imL f & f (inLz x) = z. pose f0 := kHomExtend 1 \1 (inLz x) z. have{map1q1z_z} hom_f0 : kHom 1 <<1; inLz x>> f0. by apply: kHomExtendP map1q1z_z => //; apply: kHom1. - have{splitLpz} splitLpz: splittingFieldFor <<1; inLz x>> pz imL. + have{} splitLpz: splittingFieldFor <<1; inLz x>> pz imL. have [r def_pz defLz] := splitLpz; exists r => //. apply/eqP; rewrite eqEsubv -{2}defLz adjoin_seqSl ?sub1v // andbT. apply/Fadjoin_seqP; split; last first. @@ -1230,7 +1230,7 @@ exists (pmap f r). rewrite splitKa; have{splitKa}: all (root (minPoly K a)) r. by apply/allP => b; rewrite splitKa root_prod_XsubC. elim: r Er => /= [|b r IHr]; first by rewrite !big_nil. -case/andP=> Eb Er /andP[pKa_b_0 /(IHr Er){IHr Er}IHr]. +case/andP=> Eb Er /andP[pKa_b_0 /(IHr Er){Er}IHr]. have [x galE /eqP xa_b] := normalField_root_minPoly sKE nKE Ea pKa_b_0. rewrite /(f b); case: (pickP _) => [y /andP[_ /eqP<-]|/(_ x)/andP[]//]. by rewrite !big_cons IHr. @@ -1587,7 +1587,7 @@ Proof. by rewrite -normalField_ker ker_normal. Qed. Lemma normalField_img : normalField_cast @* 'Gal(E / K) = 'Gal(M / K). Proof. have [[sKM sME] [sKE _ nKE]] := (andP sKME, and3P galKE). -apply/setP=> x; apply/idP/idP=> [/morphimP[{x}x galEx _ ->] | galMx]. +apply/setP=> x; apply/idP/idP=> [/morphimP[{}x galEx _ ->] | galMx]. rewrite gal_kHom //; apply/kAHomP=> a Ka; have Ma := subvP sKM a Ka. by rewrite normalField_cast_eq // (fixed_gal sKE). have /(kHom_to_gal sKME nKE)[y galEy eq_xy]: kHom K M x by rewrite -gal_kHom. diff --git a/mathcomp/field/separable.v b/mathcomp/field/separable.v index e51a660..6320343 100644 --- a/mathcomp/field/separable.v +++ b/mathcomp/field/separable.v @@ -414,7 +414,7 @@ exists p => //; exists (\poly_(i < r.+1) f`_(i * p)). rewrite comp_polyE size_poly_eq -?Dn ?fn1 ?oner_eq0 //. have pr_p := charf_prime charLp; have p_gt0 := prime_gt0 pr_p. apply/polyP=> i; rewrite coef_sum. -have [[{i} i ->] | p'i] := altP (@dvdnP p i); last first. +have [[{}i ->] | p'i] := altP (@dvdnP p i); last first. rewrite big1 => [|j _]; last first. rewrite coefZ -exprM coefXn [_ == _](contraNF _ p'i) ?mulr0 // => /eqP->. by rewrite dvdn_mulr. @@ -512,7 +512,7 @@ Lemma Derivation_separableP : (separable_element K x). Proof. apply: (iffP idP) => [sepKx D derD /subvP DK_0 | derKx_0]. - have{DK_0} DK_0 q: q \is a polyOver K -> map_poly D q = 0. + have{} DK_0 q: q \is a polyOver K -> map_poly D q = 0. move=> /polyOverP Kq; apply/polyP=> i; apply/eqP. by rewrite coef0 coef_map -memv_ker DK_0. apply/subvP=> _ /Fadjoin_polyP[p Kp ->]; rewrite memv_ker. @@ -771,7 +771,7 @@ have sep_pKy: separable_poly (minPoly K y). have{sep_pKy} sep_q: separable_poly q by rewrite Dq separable_map in sep_pKy. have [r nz_r PETr] := large_field_PET nz_p px0 qy0 sep_q. have [[s [Us Ks /ltnW leNs]] | //] := finite_PET (size r). -have{s Us leNs} /allPn[t {Ks}/Ks Kt nz_rt]: ~~ all (root r) s. +have{s Us leNs} /allPn[t {}/Ks Kt nz_rt]: ~~ all (root r) s. by apply: contraTN leNs; rewrite -ltnNge => /max_poly_roots->. have{PETr} [/= [p1 Dx] [q1 Dy]] := PETr (Subvs Kt) nz_rt. set z := t * y - x in Dx Dy; exists z; apply/eqP. |