Adapt to https://github.com/math-comp/math-comp/pull/1201

theories/abel.v

@@ -310,7 +310,7 @@
   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 @@
 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.
@@ -902,12 +902,12 @@
 Proof.
 have := p_irr; rewrite /irreducible_poly => -[+ _].
 by apply: contraTneq => ->; rewrite size_poly0.
 Qed.
 
 Let ratr_p' : map_poly ratr p %= \prod_(x <- rp') ('X - x%:P).
 Proof.
 by have := poly_numfield_eqp p_neq0; rewrite (eq_map_poly (fmorph_eq_rat _)).
 Qed.
 
 Let rp'_uniq : uniq rp'.
 Proof.
@@ -917,7 +917,7 @@
 rewrite size_poly_eq1; have [//|dN1 /(_ isT)] := boolP (d %= 1).
 move=> /eqp_dvdl-> /dvdp_leq; rewrite -size_poly_eq0 polyorder.size_deriv.
 by case: (size p) sp_gt1 => [|[|n]]//= _; rewrite ltnn; apply.
 Qed.
 
 Let d := (size p).-1.
 Hypothesis d_prime : prime d.
@@ -926,8 +926,8 @@
 Let rp := [seq x <- rp' | iota x \isn't Num.real]
           ++ [seq x <- rp' | iota x \is Num.real].
 
 Let rp_perm : perm_eq rp rp'. Proof. by rewrite perm_catC perm_filterC. Qed.
 Let rp_uniq : uniq rp. Proof. by rewrite (perm_uniq rp_perm). Qed.
 Let ratr_p : map_poly ratr p %= \prod_(x <- rp) ('X - x%:P).
 Proof.
 rewrite (eqp_trans ratr_p')// eqp_monic ?monic_prod_XsubC//.
@@ -1286,7 +1286,7 @@
 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.
@@ -1322,11 +1322,11 @@
 have p1  : Num.sg pR.[1%:~R]        = - 1 by rewrite pRE !pesimp -lock rmorphN1.
 have p2  : Num.sg pR.[2%:~R]        =   1 by rewrite pRE !pesimp -lock rmorph1.
 have simp := (pN2, pN1, p1, p2, mulN1r, mulrN1).
 have [||x0 /andP[_ x0N1] rx0] := @ivt_sign _ pR (- 2%:R) (- 1); rewrite ?simp//.
   by rewrite -subr_ge0 opprK addKr ler01.
 have [||x1 /andP[x10 x11] rx1] := @ivt_sign _ pR (-1) 1; rewrite ?simp//.
   by rewrite -subr_ge0 opprK addr_ge0 ?ler01.
 have [||x2 /andP[/= x21 _] rx2] := @ivt_sign _ pR 1 2%:R; rewrite ?simp//.
   by rewrite -subr_ge0 addrK ler01.
 have: sorted <%R [:: x0; x1; x2] by rewrite /= (lt_trans x0N1) ?(lt_trans x11).
 rewrite lt_sorted_uniq_le => /andP[uniqx012 _].
@@ -1502,7 +1502,7 @@
   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 @@
   + 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).

theories/xmathcomp/algR.v

@@ -35,7 +35,7 @@
 
 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.
@@ -65,14 +65,14 @@
 
 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.
 Qed.
 HB.instance Definition _ := Num.RealField_isArchimedean.Build algR
   algR_archiFieldMixin.
 
 Definition algRpfactor (x : algC) : {poly algR} :=
@@ -135,7 +135,7 @@
 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.

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.
 

theories/xmathcomp/cyclotomic_ext.v

@@ -63,7 +63,7 @@
 have ePp : P n * p = 'X^n - 1 by rewrite -eP fact.
 have eQq : Q n * q = 'X^n - 1 by rewrite -eQ fact.
 have Xnsub1N0 : 'X^n - 1 != 0 :> {poly F}.
   by rewrite -size_poly_gt0 size_Xn_sub_1.
 have pN0 : p != 0 by apply: dvdpN0 Xnsub1N0; rewrite -ePp dvdp_mulIr.
 have epq : p = q.
   case: (divisors_correct n_gt0) => uniqd sortedd dP.
@@ -157,7 +157,7 @@
 have h1_in : (h ^-1)%g \in 'Gal(<<E; w>> / 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.