From b4b4752f889c29717bcf858a6a5d9c065c691607 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Mon, 8 Apr 2024 10:50:56 +0200 Subject: [PATCH] Adapt to https://github.com/math-comp/math-comp/pull/1207 --- theories/abel.v | 12 ++++++------ theories/xmathcomp/algR.v | 6 +++--- theories/xmathcomp/char0.v | 2 +- theories/xmathcomp/cyclotomic_ext.v | 2 +- 4 files changed, 11 insertions(+), 11 deletions(-) diff --git a/theories/abel.v b/theories/abel.v index b0ff1cf..cf6694d 100644 --- a/theories/abel.v +++ b/theories/abel.v @@ -310,7 +310,7 @@ suff -> : F = <>%AS. apply: radical_ext_Fadjoin n_gt0 _. rewrite -(galois_fixedField galois_EF) -/G GE. apply/fixedFieldP; first by rewrite rpredX. - move=> _ /cycleP[i ->]; rewrite rmorphX/= gXx exprMn exprVn exprAC. + move=> _ /cycleP[i ->]; rewrite rmorphXn/= gXx exprMn exprVn exprAC. by rewrite (prim_expr_order w_root)// expr1n invr1 mul1r. apply/val_inj/eqP => /=. have -> : F = fixedField (1%g : {set gal_of F}) :> {vspace L}. @@ -533,7 +533,7 @@ Proof. move=> p_prime p_neq0 xpE; have p_gt0 := prime_gt0 p_prime. wlog [w w_root] : L E x xpE / {w : L | p.-primitive_root w} => [hwlog|]. apply: (@classic_cycloSplitting _ L p p_neq0) => -[L' [w [f wf rw]]]. - rewrite -(solvable_ext_aimg f) aimg_adjoin hwlog -?rmorphX ?memv_img//. + rewrite -(solvable_ext_aimg f) aimg_adjoin hwlog -?rmorphXn ?memv_img//. by exists w. have galEw := galois_Fadjoin_cyclotomic E w_root. have solEw := solvable_Fadjoin_cyclotomic E w_root. @@ -1286,7 +1286,7 @@ rewrite deriv_poly_example /root. rewrite rmorphB /= linearZ map_polyC/= map_polyXn !pesimp. rewrite -[5%:R]sqr_sqrtr ?ler0n// (exprM _ 2 2) -exprMn (natrX _ 2 2) subr_sqr. rewrite mulf_eq0 [_ + 2%:R == 0]gt_eqF ?orbF; last first. - by rewrite ltr_spaddr ?ltr0n// mulr_ge0 ?sqrtr_ge0// exprn_even_ge0. + by rewrite ltr_pwDr ?ltr0n// mulr_ge0 ?sqrtr_ge0// exprn_even_ge0. have sqrt5N0 : Num.sqrt (5%:R : algR) != 0 by rewrite gt_eqF// sqrtr_gt0 ?ltr0n. rewrite subr_eq0 (can2_eq (mulKf _) (mulVKf _))// mulrC -subr_eq0. rewrite -[X in _ - X]sqr_sqrtr; last first. @@ -1502,7 +1502,7 @@ have Cchar := Cchar => p_neq0; split. move=> /radicalP[]; case: i => // i in epw * => _ uik. pose v := i.+1.-root (iota (u ^+ i.+1)). have : ('X ^+ i.+1 - (v ^+ i.+1)%:P).[iota u] == 0. - by rewrite !hornerE ?hornerXn rootCK// rmorphX subrr. + by rewrite !hornerE ?hornerXn rootCK// rmorphXn subrr. (* FIXME: remove ?hornerXn when requiring MC >= 1.16.0 *) have /Xn_sub_xnE->// := prim1rootP (isT : 0 < i.+1)%N. rewrite horner_prod prodf_seq_eq0/= => /hasP[/= l _]. @@ -1614,10 +1614,10 @@ elim: f => //= [x|c|u f1 IHf1|b f1 IHf1 f2 IHf2] in k {r fr} als1 als1E *. + rewrite (Fadjoin_idP _); first exact: rext_refl. by have /fmorph_inj-> := IHl; rewrite rpredV. + rewrite (Fadjoin_idP _); first exact: rext_refl. - by have := IHl; rewrite -rmorphX => /fmorph_inj->; rewrite rpredX. + by have := IHl; rewrite -rmorphXn => /fmorph_inj->; rewrite rpredX. apply/(@rext_r _ _ _ n.+1)/radicalP; split => //. have /(congr1 ((@GRing.exp _)^~ n.+1)) := IHl. - by rewrite rootCK// -rmorphX => /fmorph_inj->. + by rewrite rootCK// -rmorphXn => /fmorph_inj->. - case: als1 als1E => //= a l [IHl IHlu]. rewrite -(eq_adjoin _ (mem_rcons _ _)) adjoin_rcons. pose n := size (subeval ratr f1); rewrite -[l](cat_take_drop n). diff --git a/theories/xmathcomp/algR.v b/theories/xmathcomp/algR.v index cd98e39..0f02339 100644 --- a/theories/xmathcomp/algR.v +++ b/theories/xmathcomp/algR.v @@ -35,7 +35,7 @@ HB.instance Definition _ := GRing.isMultiplicative.Build algR algC algRval Definition algR_norm (x : algR) : algR := in_algR (normr_real (val x)). Lemma algR_ler_norm_add x y : algR_norm (x + y) <= (algR_norm x + algR_norm y). -Proof. exact: ler_norm_add. Qed. +Proof. exact: ler_normD. Qed. Lemma algR_normr0_eq0 x : algR_norm x = 0 -> x = 0. Proof. by move=> /(congr1 val)/normr0_eq0 ?; apply/val_inj. Qed. Lemma algR_normrMn x n : algR_norm (x *+ n) = algR_norm x *+ n. @@ -67,7 +67,7 @@ Definition algR_archiFieldMixin : Num.archimedean_axiom algR. Proof. move=> /= x; have /andP[/= _] := floorC_itv (valP `|x|). set n := floorC _; have [n_lt0|n_ge0] := ltP n 0. - move=> /(@lt_le_trans _ _ _ _ 0); rewrite lerz0 lez_addr1. + move=> /(@lt_le_trans _ _ _ _ 0); rewrite lerz0 lezD1. by move=> /(_ n_lt0); rewrite normr_lt0. move=> x_lt; exists (`|(n + 1)%R|%N); apply: lt_le_trans x_lt _. by rewrite /= rmorphMn/= pmulrn gez0_abs// addr_ge0. @@ -135,7 +135,7 @@ Lemma algCpfactorCgt0 x y : x \isn't Num.real -> y \is Num.real -> Proof. move=> xNR yR; rewrite algCpfactorCE// hornerM !hornerXsubC. rewrite [x]algCrect conjC_rect ?Creal_Re ?Creal_Im// !opprD !addrA opprK. -rewrite -subr_sqr exprMn sqrCi mulN1r opprK ltr_paddl//. +rewrite -subr_sqr exprMn sqrCi mulN1r opprK ltr_wpDl//. - by rewrite real_exprn_even_ge0// ?rpredB// ?Creal_Re. by rewrite real_exprn_even_gt0 ?Creal_Im ?orTb//=; apply/eqP/Creal_ImP. Qed. diff --git a/theories/xmathcomp/char0.v b/theories/xmathcomp/char0.v index e6b5c1c..14f63bc 100644 --- a/theories/xmathcomp/char0.v +++ b/theories/xmathcomp/char0.v @@ -112,7 +112,7 @@ Lemma char0_ratr_prod I r (P : pred I) E : Proof. exact: rmorph_prod. Qed. Lemma char0_ratrX n : {morph ratrL : x / x ^+ n}. -Proof. exact: rmorphX. Qed. +Proof. exact: rmorphXn. Qed. Lemma char0_nat n : ratrL n%:R = n%:R. Proof. exact: ratr_nat. Qed. diff --git a/theories/xmathcomp/cyclotomic_ext.v b/theories/xmathcomp/cyclotomic_ext.v index 35eb025..459c06d 100644 --- a/theories/xmathcomp/cyclotomic_ext.v +++ b/theories/xmathcomp/cyclotomic_ext.v @@ -157,7 +157,7 @@ have := svalP (prim_rootP w_is_nth_root (hg_gal _ g_in)). have h1_in : (h ^-1)%g \in 'Gal(<> / E)%g by rewrite ?groupV. have := svalP (prim_rootP w_is_nth_root (hg_gal _ h1_in)). set ih1 := sval _ => hh1; set ig := sval _ => hg. -rewrite hh1 rmorphX /= hg exprAC -hh1 rmorphX /=. +rewrite hh1 rmorphXn /= hg exprAC -hh1 rmorphXn /=. by rewrite -galM ?memv_adjoin // mulVg gal_id. Qed.