Switch from long suffixes to short suffixes

4 files changed, 7 insertions, 8 deletions

diff --git a/mathcomp/character/inertia.v b/mathcomp/character/inertia.v
index 76535fa..29d7162 100644
--- a/mathcomp/character/inertia.v
+++ b/mathcomp/character/inertia.v
@@ -1492,7 +1492,7 @@ have kerN_mu_t: N \subset cfker (mu / 'chi_t)%R.
   by rewrite /= uNlam tNlam divrr ?lin_char_unitr ?cfker_cfun1.
 have co_e_mu_t: coprime e #[(mu / 'chi_t)%R]%CF.
   suffices dv_o_mu_t: #[(mu / 'chi_t)%R]%CF %| 'o(mu)%CF * 'o('chi_t)%CF.
-    by rewrite (coprime_dvdr dv_o_mu_t) // coprime_mulr o_mu co_e_lam.
+    by rewrite (coprime_dvdr dv_o_mu_t) // coprimeMr o_mu co_e_lam.
   rewrite !cfDet_order_lin //; apply/dvdn_cforderP=> x Gx.
   rewrite invr_lin_char // !cfunE exprMn -rmorphX {2}mulnC.
   by rewrite !(dvdn_cforderP _) ?conjC1 ?mulr1 // dvdn_mulr.
@@ -1513,7 +1513,7 @@ Corollary extend_solvable_coprime_irr G N t (theta := 'chi[N]_t) :
                 d = c].
 Proof.
 set e := #|G : N|; set f := truncC _ => nsNG solG IGtheta.
-rewrite coprime_mulr => /andP[co_e_th co_e_f].
+rewrite coprimeMr => /andP[co_e_th co_e_f].
 have [sNG nNG] := andP nsNG; pose lambda := cfDet theta.
 have lin_lam: lambda \is a linear_char := cfDet_lin_char theta.
 have IGlam: G \subset 'I[lambda].
diff --git a/mathcomp/character/integral_char.v b/mathcomp/character/integral_char.v
index c603f91..c82202b 100644
--- a/mathcomp/character/integral_char.v
+++ b/mathcomp/character/integral_char.v
@@ -341,7 +341,7 @@ have p_dvd_supp_g i: ~~ p_dv1 i && (i != 0) -> 'chi_i g = 0.
     rewrite fful_i subG1 -(isog_eq1 (isog_center (quotient1_isog G))) /=.
     by rewrite trivZ.
   rewrite coprime_degree_support_cfcenter ?trivZi ?inE //.
-  by rewrite -/m Dm irr1_degree natCK coprime_sym coprime_expl.
+  by rewrite -/m Dm irr1_degree natCK coprime_sym coprimeXl.
 pose alpha := \sum_(i | p_dv1 i && (i != 0)) 'chi_i 1%g / p%:R * 'chi_i g.
 have nz_p: p%:R != 0 :> algC by rewrite pnatr_eq0 -lt0n prime_gt0.
 have Dalpha: alpha = - 1 / p%:R.
@@ -592,7 +592,7 @@ have ZchiP: 'Res[P] 'chi_i \in 'CF(P, P :&: 'Z(G)).
   apply/cfun_onP=> x; rewrite inE; have [Px | /cfun0->//] := boolP (x \in P).
   rewrite /= -(cfcenter_fful_irr fful_i) cfResE //.
   apply: coprime_degree_support_cfcenter.
-  rewrite Dchi1 coprime_expl // prime_coprime // -p'natE //.
+  rewrite Dchi1 coprimeXl // prime_coprime // -p'natE //.
   apply: pnat_dvd p'PiG; rewrite -index_cent1 indexgS // subsetI sPG.
   by rewrite sub_cent1 (subsetP cPP).
 have /andP[_ nZG] := center_normal G; have nZP := subset_trans sPG nZG.
diff --git a/mathcomp/character/mxabelem.v b/mathcomp/character/mxabelem.v
index 92470d9..949ded3 100644
--- a/mathcomp/character/mxabelem.v
+++ b/mathcomp/character/mxabelem.v
@@ -469,7 +469,7 @@ Local Notation rVn := 'rV['F_p](gval E).
 Lemma dim_abelemE : n = logn p #|E|.
 Proof.
 rewrite /n'; have [_ _ [k ->]] :=  pgroup_pdiv pE ntE.
-by rewrite /pdiv primes_exp ?primes_prime // pfactorK.
+by rewrite /pdiv primesX ?primes_prime // pfactorK.
 Qed.
 
 Lemma card_abelem_rV : #|rVn| = #|E|.
diff --git a/mathcomp/character/mxrepresentation.v b/mathcomp/character/mxrepresentation.v
index 51d28f8..e94e69f 100644
--- a/mathcomp/character/mxrepresentation.v
+++ b/mathcomp/character/mxrepresentation.v
@@ -4908,8 +4908,7 @@ Proof.
 rewrite map_kermx //; congr (kermx _); apply: map_lin1_mx => //= v.
 rewrite map_mxvec map_mxM; congr (mxvec (_ *m _)); last first.
   by apply: map_lin1_mx => //= u; rewrite map_mxM map_vec_mx.
-apply/row_matrixP=> i.
-by rewrite -map_row !rowK map_mxvec map_mx_sub map_mx1.
+by apply/row_matrixP=> i; rewrite -map_row !rowK map_mxvec map_mxB map_mx1.
 Qed.
 
 Lemma rcent_map A : rcent rGf A^f = rcent rG A.
@@ -4990,7 +4989,7 @@ rewrite {1}in_submodE mulmxA -in_submodE -in_submodJ; last first.
   by rewrite genmxE -(in_factmod_addsK _ V^f) submxMr.
 congr (in_submod _ _); rewrite -in_factmodJ // in_factmodE mulmxA -in_factmodE.
 apply/eqP; rewrite -subr_eq0 -def_rGf -!map_mxM -linearB in_factmod_eq0.
-rewrite -map_mx_sub map_submx -in_factmod_eq0 linearB.
+rewrite -map_mxB map_submx -in_factmod_eq0 linearB.
 rewrite /= (in_factmodJ modU) // val_factmodK.
 rewrite [valUV]val_factmodE mulmxA -val_factmodE val_factmodK.
 rewrite -val_submodE in_submodK ?subrr //.