running semi-automated linting on the whole library

7 files changed, 59 insertions, 59 deletions

diff --git a/mathcomp/character/character.v b/mathcomp/character/character.v
index 0738b14..6408b0b 100644
--- a/mathcomp/character/character.v
+++ b/mathcomp/character/character.v
@@ -382,7 +382,7 @@ Lemma prod_repr_lin n2 (rG1 : reprG 1) (rG2 : reprG n2) :
   {in G, forall x, let cast_n2 := esym (mul1n n2) in
       prod_repr rG1 rG2 x = castmx (cast_n2, cast_n2) (rG1 x 0 0 *: rG2 x)}.
 Proof.
-move=> x Gx /=; set cast_n2 := esym _; rewrite /prod_repr /= !mxE !lshift0.      
+move=> x Gx /=; set cast_n2 := esym _; rewrite /prod_repr /= !mxE !lshift0.
 apply/matrixP=> i j; rewrite castmxE /=.
 do 2![rewrite mxE; case: splitP => [? ? | []//]].
 by congr ((_ *: rG2 x) _ _); apply: val_inj.
@@ -511,7 +511,7 @@ Proof. by move=> A B; rewrite /xcfun linearB mulmxBl !mxE. Qed.
 Canonical xcfun_additive phi := Additive (xcfun_is_additive phi).
 
 Lemma xcfunZr a phi A : xcfun phi (a *: A) = a * xcfun phi A.
-Proof. by rewrite /xcfun linearZ -scalemxAl mxE. Qed. 
+Proof. by rewrite /xcfun linearZ -scalemxAl mxE. Qed.
 
 (* In order to add a second canonical structure on xcfun *)
 Definition xcfun_r_head k A phi := let: tt := k in xcfun phi A.
@@ -530,7 +530,7 @@ Lemma xcfunZl a phi A : xcfun (a *: phi) A = a * xcfun phi A.
 Proof.
 rewrite /xcfun !mxE big_distrr; apply: eq_bigr => i _ /=.
 by rewrite !mxE cfunE mulrCA.
-Qed. 
+Qed.
 
 Lemma xcfun_repr n rG A : xcfun (@cfRepr n rG) A = \tr (gring_op rG A).
 Proof.
@@ -1431,7 +1431,7 @@ Proof.
 apply/eqP/andP=> [|[/eqP-> /pred2P[]-> //]]; last by rewrite !scale0r.
 move/(congr1 (cfdotr 'chi__)) => /= eq_ai_bj.
 move: {eq_ai_bj}(eq_ai_bj i) (esym (eq_ai_bj j)); rewrite !cfdotZl !cfdot_irr.
-by rewrite !mulr_natr !mulrb !eqxx eq_sym orbC; case: ifP => _ -> //= ->. 
+by rewrite !mulr_natr !mulrb !eqxx eq_sym orbC; case: ifP => _ -> //= ->.
 Qed.
 
 Lemma eq_signed_irr (s t : bool) i j :
@@ -1624,7 +1624,7 @@ have:= (normC_sum_upper _ Kx) i; rewrite !cfunE => -> // {i Ci} i _.
 have chi_i_ge0: 0 <= '[chi, 'chi_i].
   by rewrite Cnat_ge0 ?Cnat_cfdot_char_irr.
 by rewrite !cfunE normrM (normr_idP _) ?ler_wpmul2l ?char1_ge_norm ?irr_char.
-Qed. 
+Qed.
 
 Lemma TI_cfker_irr : \bigcap_i cfker 'chi[G]_i = [1].
 Proof.
@@ -1710,7 +1710,7 @@ Lemma cfRes_irr_irr chi :
   chi \is a character -> 'Res[H] chi \in irr H -> chi \in irr G.
 Proof.
 have [sHG /char_reprP[rG ->] | not_sHG Nchi] := boolP (H \subset G).
-  rewrite -(cfRepr_sub _ sHG) => /irr_reprP[rH irrH def_rH]; apply/irr_reprP. 
+  rewrite -(cfRepr_sub _ sHG) => /irr_reprP[rH irrH def_rH]; apply/irr_reprP.
   suffices /subg_mx_irr: mx_irreducible (subg_repr rG sHG) by exists rG.
   by apply: mx_rsim_irr irrH; apply/cfRepr_rsimP/eqP.
 rewrite cfResEout // => /irrP[j Dchi_j]; apply/lin_char_irr/cfRes_lin_lin=> //.
@@ -2152,7 +2152,7 @@ Lemma cfBigdprod_eq1 phi :
 Proof.
 move=> Nphi; set Phi := cfBigdprod defG phi.
 apply/eqP/eqfun_inP=> [Phi1 i Pi | phi1]; last first.
-  by apply: big1 => i /phi1->; rewrite rmorph1. 
+  by apply: big1 => i /phi1->; rewrite rmorph1.
 have Phi1_1: Phi 1%g = 1 by rewrite Phi1 cfun1E group1.
 have nz_Phi1: Phi 1%g != 0 by rewrite Phi1_1 oner_eq0.
 have [_ <-] := cfBigdprodK nz_Phi1 Pi.
@@ -2484,7 +2484,7 @@ Lemma lin_char_group G :
              {morph cF : u v / (u * v)%g >-> (u * v)%R},
              forall k, {morph cF : u / (u^+ k)%g >-> u ^+ k},
              {morph cF: u / u^-1%g >-> u^-1%CF}
-           & {mono cF: u / #[u]%g >-> #[u]%CF} ]}}. 
+           & {mono cF: u / #[u]%g >-> #[u]%CF} ]}}.
 Proof.
 pose linT := {i : Iirr G | 'chi_i \is a linear_char}.
 pose cF (u : linT) := 'chi_(sval u).
@@ -2567,7 +2567,7 @@ Variables (n : nat) (rG : mx_representation [fieldType of algC] G n).
 
 Definition det_repr_mx x : 'M_1 := (\det (rG x))%:M.
 
-Fact det_is_repr : mx_repr G det_repr_mx. 
+Fact det_is_repr : mx_repr G det_repr_mx.
 Proof.
 split=> [|g h Gg Gh]; first by rewrite /det_repr_mx repr_mx1 det1.
 by rewrite /det_repr_mx repr_mxM // det_mulmx !mulmxE scalar_mxM.
@@ -2725,7 +2725,7 @@ apply/eqP/is_scalar_mxP=> [|[c rG_c]].
   by case/max_cfRepr_norm_scalar=> // c; exists c.
 rewrite -(sqrCK (char1_ge0 (cfRepr_char rG))) normC_def; congr (sqrtC _).
 rewrite expr2 -{2}(mulgV x) -char_inv ?cfRepr_char ?cfunE ?groupM ?groupV //.
-rewrite  Gx group1 repr_mx1 repr_mxM ?repr_mxV ?groupV // !mulrb rG_c.
+rewrite Gx group1 repr_mx1 repr_mxM ?repr_mxV ?groupV // !mulrb rG_c.
 by rewrite invmx_scalar -scalar_mxM !mxtrace_scalar mulrnAr mulrnAl mulr_natl.
 Qed.
 
diff --git a/mathcomp/character/classfun.v b/mathcomp/character/classfun.v
index 54cbc41..81c26ab 100644
--- a/mathcomp/character/classfun.v
+++ b/mathcomp/character/classfun.v
@@ -464,7 +464,7 @@ Notation "{ 'in' CFD , 'isometry' tau , 'to' CFR }" :=
   (at level 0, format "{ 'in'  CFD ,  'isometry'  tau ,  'to'  CFR }")
      : type_scope.
 
-Section ClassFun. 
+Section ClassFun.
 
 Variables (gT : finGroupType) (G : {group gT}).
 Implicit Types (A B : {set gT}) (H K : {group gT}) (phi psi xi : 'CF(G)).
@@ -1123,7 +1123,7 @@ Qed.
 Lemma eq_pairwise_orthogonal R S :
   perm_eq R S -> pairwise_orthogonal R = pairwise_orthogonal S.
 Proof.
-apply: catCA_perm_subst R S => R S S'. 
+apply: catCA_perm_subst R S => R S S'.
 rewrite !pairwise_orthogonal_cat !orthogonal_catr (orthogonal_sym R S) -!andbA.
 by do !bool_congr.
 Qed.
@@ -1201,7 +1201,7 @@ Qed.
 Lemma sub_orthonormal S1 S2 :
   {subset S1 <= S2} -> uniq S1 -> orthonormal S2 -> orthonormal S1.
 Proof.
-move=> sS12 uniqS1 /orthonormalP[_ oS1]. 
+move=> sS12 uniqS1 /orthonormalP[_ oS1].
 by apply/orthonormalP; split; last apply: sub_in2 sS12 _ _.
 Qed.
 
@@ -1386,7 +1386,7 @@ Qed.
 
 Lemma cfRes_is_multiplicative : multiplicative cfRes.
 Proof.
-split=> [phi psi|]; [apply/cfunP=> x | exact: cfRes_cfun1]. 
+split=> [phi psi|]; [apply/cfunP=> x | exact: cfRes_cfun1].
 by rewrite !cfunElock mulrnAr mulrnAl -mulrnA mulnb andbb.
 Qed.
 Canonical cfRes_rmorphism := AddRMorphism cfRes_is_multiplicative.
@@ -1489,7 +1489,7 @@ Canonical cfMorph_linear := Linear cfMorph_is_linear.
 
 Fact cfMorph_is_multiplicative : multiplicative cfMorph.
 Proof.
-split=> [phi psi|]; [apply/cfunP=> x | exact: cfMorph_cfun1]. 
+split=> [phi psi|]; [apply/cfunP=> x | exact: cfMorph_cfun1].
 by rewrite !cfunElock mulrnAr mulrnAl -mulrnA mulnb andbb.
 Qed.
 Canonical cfMorph_rmorphism := AddRMorphism cfMorph_is_multiplicative.
@@ -1567,7 +1567,7 @@ Canonical cfIsom_unlockable := [unlockable of cfIsom].
 
 Lemma cfIsomE phi x : x \in G -> cfIsom phi (f x) = phi x.
 Proof.
-move=> Gx; rewrite unlock cfMorphE //= /restrm ?defG ?cfRes_id ?invmE //. 
+move=> Gx; rewrite unlock cfMorphE //= /restrm ?defG ?cfRes_id ?invmE //.
 by rewrite -defR mem_morphim.
 Qed.
 
@@ -1751,7 +1751,7 @@ Lemma sub_cfker_mod (A : {set gT}) K (psi : 'CF(G / K)) :
   (A \subset cfker (psi %% K)) = (A / K \subset cfker psi)%g.
 Proof.
 by move=> nsKG nKA; rewrite -(quotientSGK nKA) ?quotient_cfker_mod ?cfker_mod.
-Qed.  
+Qed.
 
 Lemma cfker_quo H phi :
   H <| G -> H \subset cfker (phi) -> cfker (phi / H) = (cfker phi / H)%g.
@@ -1872,7 +1872,7 @@ Proof. by apply: cforder_inj_rmorph cfSdprod_inj. Qed.
 
 End SDproduct.
 
-Section DProduct. 
+Section DProduct.
 
 Variables (gT : finGroupType) (G K H : {group gT}).
 Hypothesis KxH : K \x H = G.
@@ -2065,7 +2065,7 @@ by rewrite -[P j](mem_enum P) r_j.
 Qed.
 
 Lemma cfBigdprodi_iso i : P i -> isometry (@cfBigdprodi i).
-Proof. by move=> Pi phi psi; rewrite cfDprodl_iso Pi !cfRes_id. Qed. 
+Proof. by move=> Pi phi psi; rewrite cfDprodl_iso Pi !cfRes_id. Qed.
 
 Definition cfBigdprod (phi : forall i, 'CF(A i)) :=
   \prod_(i | P i) cfBigdprodi (phi i).
@@ -2321,7 +2321,7 @@ Lemma cfIndM phi psi:  H \subset G ->
 Proof.
 move=> HsG; apply/cfun_inP=> x Gx; rewrite !cfIndE // !cfunE !cfIndE // -mulrA.
 congr (_ * _); rewrite mulr_suml; apply: eq_bigr=> i iG; rewrite !cfunE.
-case:(boolP (x^i \in H))=> xJi; last by rewrite cfun0gen ?mul0r ?genGid.
+case: (boolP (x^i \in H))=> xJi; last by rewrite cfun0gen ?mul0r ?genGid.
 by rewrite !cfResE //; congr (_*_); rewrite cfunJgen ?genGid.
 Qed.
 
diff --git a/mathcomp/character/inertia.v b/mathcomp/character/inertia.v
index 3890fdd..9ae289d 100644
--- a/mathcomp/character/inertia.v
+++ b/mathcomp/character/inertia.v
@@ -277,7 +277,7 @@ Qed.
 
 Lemma inertia_scale a phi : 'I[phi] \subset 'I[a *: phi].
 Proof.
-apply/subsetP=> x /setIdP[nHx /eqP Iphi_x]. 
+apply/subsetP=> x /setIdP[nHx /eqP Iphi_x].
 by rewrite inE nHx linearZ /= Iphi_x.
 Qed.
 
@@ -497,7 +497,7 @@ Lemma cfResInd j:
 Proof.
 case/andP=> [sHG /subsetP nHG].
 rewrite (reindex_inj invg_inj); apply/cfun_inP=> x Hx.
-rewrite  cfResE // cfIndE // ?cfunE ?sum_cfunE; congr (_ * _).
+rewrite cfResE // cfIndE // ?cfunE ?sum_cfunE; congr (_ * _).
 by apply: eq_big => [y | y Gy]; rewrite ?cfConjgE ?groupV ?invgK ?nHG.
 Qed.
 
@@ -933,7 +933,7 @@ have AtoB_P s (psi := 'chi_s) (chi := 'Ind[G] psi): s \in calA ->
 - rewrite !constt_Ind_Res => sHt; have [r sGr] := constt_cfInd_irr s sTG.
   have rTs: s \in irr_constt ('Res[T] 'chi_r) by rewrite -constt_Ind_Res.
   have NrT: 'Res[T] 'chi_r \is a character by rewrite cfRes_char ?irr_char.
-  have rHt: t \in irr_constt ('Res[H] 'chi_r). 
+  have rHt: t \in irr_constt ('Res[H] 'chi_r).
     by have:= constt_Res_trans NrT rTs sHt; rewrite cfResRes.
   pose e := '['Res[H] 'chi_r, theta]; set f := '['Res[H] psi, theta].
   have DrH: 'Res[H] 'chi_r = e *: \sum_(xi <- (theta ^: G)%CF) xi.
@@ -956,7 +956,7 @@ have AtoB_P s (psi := 'chi_s) (chi := 'Ind[G] psi): s \in calA ->
     rewrite (mono_lerif (ler_pmul2r (irr1_gt0 t))); apply: lerif_eq.
     by rewrite /e -(cfResRes _ sHT) ?cfdot_Res_ge_constt.
   have [_ /esym] := lerif_trans ub_chi_r lb_chi_r; rewrite eqxx.
-  by case/andP=> /eqP Dchi /eqP->;rewrite cfIirrE -/chi -?Dchi ?mem_irr.
+  by case/andP=> /eqP Dchi /eqP->; rewrite cfIirrE -/chi -?Dchi ?mem_irr.
 have part_c: {in calA, forall s (chi := 'Ind[G] 'chi_s),
   [predI irr_constt ('Res[T] chi) & calA] =i pred1 s}.
 - move=> s As chi s1; have [irr_chi _ /eqP Dchi_theta] := AtoB_P s As.
@@ -987,14 +987,14 @@ exists s => //; have [/irrP[r1 DsG] _ _] := AtoB_P s As.
 by apply/eqP; rewrite /AtoB -constt_Ind_Res DsG irrK constt_irr in rTs *.
 Qed.
 
-End ConsttInertiaBijection. 
+End ConsttInertiaBijection.
 
 Section ExtendInvariantIrr.
 
 Variable gT : finGroupType.
 Implicit Types G H K L M N : {group gT}.
 
-Section ConsttIndExtendible. 
+Section ConsttIndExtendible.
 
 Variables (G N : {group gT}) (t : Iirr N) (c : Iirr G).
 Let theta := 'chi_t.
@@ -1174,7 +1174,7 @@ have [inj_Mphi | /injectivePn[i [j i'j eq_mm_ij]]] := boolP (injectiveb mmLth).
   rewrite eqn_leq lt0n (contraNneq _ (irr1_neq0 s)); last first.
     by rewrite -(cfRes1 L) DthL cfunE => ->; rewrite !mul0r.
   rewrite -leq_sqr -leC_nat natrX -(ler_pmul2r (irr1_gt0 p0)) -mulrA mul1r.
-  have ->: e%:R * 'chi_p0 1%g = 'Res[L] theta 1%g by rewrite DthL cfunE. 
+  have ->: e%:R * 'chi_p0 1%g = 'Res[L] theta 1%g by rewrite DthL cfunE.
   rewrite cfRes1 -(ler_pmul2l (gt0CiG K L)) -cfInd1 // -/phi.
   rewrite -card_quotient // -card_Iirr_abelian // mulr_natl.
   rewrite ['Ind phi]cfun_sum_cfdot sum_cfunE (bigID (mem (codom mmLth))) /=.
@@ -1497,7 +1497,7 @@ have kerN_mu_t: N \subset cfker (mu / 'chi_t)%R.
   rewrite -subsetIidl -cfker_Res ?lin_charW ?rpred_div ?rmorph_div //.
   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. 
+  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.
   rewrite !cfDet_order_lin //; apply/dvdn_cforderP=> x Gx.
   rewrite invr_lin_char // !cfunE exprMn -rmorphX {2}mulnC.
@@ -1607,7 +1607,7 @@ apply: (iffP idP) => [not_chijK1 | [i nzi ->]]; last first.
 have /neq0_has_constt[i chijKi]: 'Res[K] 'chi_j != 0 by apply: Res_irr_neq0.
 have nz_i: i != 0.
   by apply: contraNneq not_chijK1 => i0; rewrite constt0_Res_cfker // -i0.
-have /irrP[k def_chik] := irr_induced_Frobenius_ker nz_i. 
+have /irrP[k def_chik] := irr_induced_Frobenius_ker nz_i.
 have: '['chi_j, 'chi_k] != 0 by rewrite -def_chik -cfdot_Res_l.
 by rewrite cfdot_irr pnatr_eq0; case: (j =P k) => // ->; exists i.
 Qed.
diff --git a/mathcomp/character/integral_char.v b/mathcomp/character/integral_char.v
index ad2980f..16e3b51 100644
--- a/mathcomp/character/integral_char.v
+++ b/mathcomp/character/integral_char.v
@@ -77,7 +77,7 @@ exists QnC => [// nuQn|].
 rewrite span_seq1 in genQn.
 exists w => // hT H phi Nphi x x_dv_n.
 apply: sig_eqW; have [rH ->] := char_reprP Nphi.
-have [Hx | /cfun0->] := boolP (x \in H); last by exists 0; rewrite rmorph0.  
+have [Hx | /cfun0->] := boolP (x \in H); last by exists 0; rewrite rmorph0.
 have [e [_ [enx1 _] [-> _] _]] := repr_rsim_diag rH Hx.
 have /fin_all_exists[k Dk] i: exists k, e 0 i = z ^+ k.
   have [|k ->] := (prim_rootP prim_z) (e 0 i); last by exists k.
@@ -657,14 +657,14 @@ have{defQn} imItoQ: calG = ItoQ @: {:I}.
 have injItoQ: {in {:I} &, injective ItoQ}.
   move=> k1 k2 _ _ /(congr1 (fun nu : gal_of _ => nu eps))/eqP.
   by apply: contraTeq; rewrite !defItoQ (eq_prim_root_expr pr_eps) !modn_small.
-pose pi1 := \prod_(s in S) chi s; pose pi2 := \prod_(s in S) `|chi s| ^+ 2. 
+pose pi1 := \prod_(s in S) chi s; pose pi2 := \prod_(s in S) `|chi s| ^+ 2.
 have Qpi1: pi1 \in Crat.
   have [a Da] := QnGg _ Nchi; suffices ->: pi1 = QnC (galNorm 1 {:Qn} a).
     have /vlineP[q ->] := mem_galNorm galQn (memvf a).
     by rewrite rmorphZ_num rmorph1 mulr1 Crat_rat.
   rewrite /galNorm rmorph_prod -/calG imItoQ big_imset //=.
   rewrite /pi1 -(eq_bigl _ _ imItoS) -big_uniq // big_map big_filter /=.
-  apply: eq_bigr => k _;  have [nuC DnuC] := gQnC (ItoQ k); rewrite DnuC Da.
+  apply: eq_bigr => k _; have [nuC DnuC] := gQnC (ItoQ k); rewrite DnuC Da.
   have [r ->] := char_sum_irr Nchi; rewrite !sum_cfunE rmorph_sum.
   apply: eq_bigr => i _; have /QnGg[b Db] := irr_char i.
   have Lchi_i: 'chi_i \is a linear_char by rewrite irr_cyclic_lin.
diff --git a/mathcomp/character/mxabelem.v b/mathcomp/character/mxabelem.v
index c178d75..92fdb0e 100644
--- a/mathcomp/character/mxabelem.v
+++ b/mathcomp/character/mxabelem.v
@@ -247,7 +247,7 @@ Lemma dprod_rowg  m1 m2 (A : 'M[F]_(m1, n)) (B : 'M[F]_(m2, n)) :
 Proof.
 rewrite (sameP mxdirect_addsP eqP) -trivg_rowg rowgI => /eqP tiAB.
 by rewrite -cprod_rowg dprodEcp.
-Qed. 
+Qed.
 
 Lemma bigcprod_rowg m I r (P : pred I) (A : I -> 'M[F]_n) (B : 'M[F]_(m, n)) :
     (\sum_(i <- r | P i) A i :=: B)%MS ->
@@ -356,7 +356,7 @@ move=> m_gt0 n_gt0 q_gt1; apply/eqP; rewrite eqn_dvd; apply/andP; split.
   apply/exponentP=> x _; apply/matrixP=> i j; rewrite mulmxnE !mxE.
   by rewrite -mulr_natr -Zp_nat_mod // modnn mulr0.
 pose cmx1 := const_mx 1%R : 'M['Z_q]_(m, n).
-apply: dvdn_trans (dvdn_exponent (in_setT cmx1)). 
+apply: dvdn_trans (dvdn_exponent (in_setT cmx1)).
 have/matrixP/(_ (Ordinal m_gt0))/(_ (Ordinal n_gt0))/eqP := expg_order cmx1.
 by rewrite mulmxnE !mxE -order_dvdn order_Zp1 Zp_cast.
 Qed.
@@ -374,7 +374,7 @@ have ->: (q ^ (m * n))%N = #|G| by rewrite cardsT card_matrix card_ord Zp_cast.
 rewrite max_card_abelian //= -grank_abelian //= -/G.
 pose B : {set 'M['Z_q]_(m, n)} := [set delta_mx ij.1 ij.2 | ij : 'I_m * 'I_n].
 suffices ->: G = <<B>>.
-  have ->: (m * n)%N = #|{: 'I_m * 'I_n}| by rewrite card_prod !card_ord. 
+  have ->: (m * n)%N = #|{: 'I_m * 'I_n}| by rewrite card_prod !card_ord.
   exact: leq_trans (grank_min _) (leq_imset_card _ _).
 apply/setP=> v; rewrite inE (matrix_sum_delta v).
 rewrite group_prod // => i _; rewrite group_prod // => j _.
@@ -770,7 +770,7 @@ move: {2}_.+1 (ltnSn (n + #|H|)) {rG G sHG}(subg_repr _ _) => m.
 elim: m gT H pH => // m IHm gT' G pG in n n_gt0 *; rewrite ltnS => le_nG_m rG.
 apply/eqP=> Gregular; have irrG: mx_irreducible rG.
   apply/mx_irrP; split=> // U modU; rewrite -mxrank_eq0 -lt0n => Unz.
-  rewrite /row_full eqn_leq rank_leq_col leqNgt; apply/negP=> ltUn. 
+  rewrite /row_full eqn_leq rank_leq_col leqNgt; apply/negP=> ltUn.
   have: rfix_mx (submod_repr modU) G != 0.
     by apply: IHm => //; apply: leq_trans le_nG_m; rewrite ltn_add2r.
   by rewrite -mxrank_eq0 (rfix_submod modU) // Gregular capmx0 linear0 mxrank0.
@@ -857,7 +857,7 @@ Theorem extraspecial_repr_structure (sS : irrType F S) :
               exists2 w, primitive_root_of_unity p w
                        & forall i, phi i z = (w ^+ i.+1)%:M
           & forall i, irr_degree (iphi i) = (p ^ n)%N]
-    & #|sS| = (p ^ n.*2 + p.-1)%N].            
+    & #|sS| = (p ^ n.*2 + p.-1)%N].
 Proof.
 have [[defPhiS defS'] prZ] := esS; set linS := linear_irr sS.
 have nb_lin: #|linS| = (p ^ n.*2)%N.
@@ -916,7 +916,7 @@ have phi_ze e: phi (z ^+ e)%g = (w ^+ e)%:M.
   by rewrite /phi irr_center_scalar ?groupX ?irr_modeX.
 have wp1: w ^+ p = 1 by rewrite -irr_modeX // -ozp expg_order irr_mode1.
 have injw: {in 'Z(S) &, injective (irr_mode i0)}.
-  move=> x y Zx Zy /= eq_xy; have [[Sx _] [Sy _]] := (setIP Zx, setIP Zy). 
+  move=> x y Zx Zy /= eq_xy; have [[Sx _] [Sy _]] := (setIP Zx, setIP Zy).
   apply: mx_faithful_inj (fful_nlin _ nlin_i0) _ _ Sx Sy _.
   by rewrite !{1}irr_center_scalar ?eq_xy; first by split.
 have prim_w e: 0 < e < p -> p.-primitive_root (w ^+ e).
diff --git a/mathcomp/character/mxrepresentation.v b/mathcomp/character/mxrepresentation.v
index 6dd4eec..0c1d4c1 100644
--- a/mathcomp/character/mxrepresentation.v
+++ b/mathcomp/character/mxrepresentation.v
@@ -712,7 +712,7 @@ Definition regular_mx x : 'M[R]_nG :=
 Lemma regular_mx_repr : mx_repr G regular_mx.
 Proof.
 split=> [|x y Gx Gy]; apply/row_matrixP=> i; rewrite !rowK.
-  by rewrite mulg1 row1 gring_valK. 
+  by rewrite mulg1 row1 gring_valK.
 by rewrite row_mul rowK -rowE rowK mulgA gring_indexK // groupM ?enum_valP.
 Qed.
 Canonical regular_repr := MxRepresentation regular_mx_repr.
@@ -1453,7 +1453,7 @@ Lemma cyclic_mx_sub m u (W : 'M_(m, n)) :
 Proof.
 move=> modU Wu; rewrite genmxE; apply/row_subP=> i.
 by rewrite row_mul mul_rV_lin1 /= mxmodule_envelop // vec_mxK row_sub.
-Qed. 
+Qed.
 
 Lemma hom_cyclic_mx u f :
   (u <= dom_hom_mx f)%MS -> (cyclic_mx u *m f :=: cyclic_mx (u *m f))%MS.
@@ -1585,7 +1585,7 @@ Proof.
 move=> isoUV [modU nzU simU]; have [f injf homUf defV] := isoUV.
 split=> [||W modW sWV nzW]; first by rewrite (mx_iso_module isoUV).
   by rewrite -(eqmx_eq0 defV) -(mul0mx n f) (can_eq (mulmxK injf)).
-rewrite -defV -[W](mulmxKV injf) submxMr //; set W' := W *m _. 
+rewrite -defV -[W](mulmxKV injf) submxMr //; set W' := W *m _.
 have sW'U: (W' <= U)%MS by rewrite -[U](mulmxK injf) submxMr ?defV.
 rewrite (simU W') //; last by rewrite -(can_eq (mulmxK injf)) mul0mx mulmxKV.
 rewrite hom_mxmodule ?dom_hom_invmx // -[W](mulmxKV injf) submxMr //.
@@ -1640,7 +1640,7 @@ Proof.
 move=> simU simV homUf sUfV nzUf; have [modU _ _] := simU.
 have [g invg homUg defUg] := mx_Schur_inj_iso simU homUf nzUf.
 exists g => //; apply: mx_Schur_onto; rewrite ?defUg //.
-by rewrite -!submx0 defUg in nzUf *. 
+by rewrite -!submx0 defUg in nzUf *.
 Qed.
 
 (* A boolean test for module isomorphism that is only valid for simple        *)
@@ -1998,7 +1998,7 @@ Proof.
 have [I [W isoUW ->]] := component_mx_def => simV homWf sVWf.
 have [i _ _|i _ ] := hom_mxsemisimple_iso simV _ homWf sVWf.
   exact: mx_iso_simple (simU).
-exact: mx_iso_trans. 
+exact: mx_iso_trans.
 Qed.
 
 Lemma component_mx_iso V : mxsimple V -> (V <= compU)%MS -> mx_iso U V.
@@ -2189,7 +2189,7 @@ have modMS: mxmodule (M :&: S)%MS by rewrite capmx_module ?subSocle_module.
 have [J /= U simU defMS _] := mxsemisimpleS modMS (capmxSr M S) ssimS.
 rewrite -defMS; apply/sumsmx_subP=> j _.
 have [sUjV sUjS]: (U j <= M /\ U j <= S)%MS.
-  by apply/andP; rewrite -sub_capmx -defMS (sumsmx_sup j). 
+  by apply/andP; rewrite -sub_capmx -defMS (sumsmx_sup j).
 have [W P_W isoWU] := subSocle_iso (simU j) sUjS.
 rewrite (sumsmx_sup W) // sub_capmx sUjV mx_iso_component //.
 exact: socle_simple.
@@ -2360,7 +2360,7 @@ suffices defM: (M == 1%:M)%MS by rewrite (eqmxP defM) mxrank1 in rM.
 case: (mx_abs_irrW absG) => _ _ ->; rewrite ?submx1 -?mxrank_eq0 ?rM //.
 apply/mxmoduleP=> x Gx; suffices: is_scalar_mx (rG x).
   by case/is_scalar_mxP=> a ->; rewrite mul_mx_scalar scalemx_sub.
-apply: (mx_abs_irr_cent_scalar absG). 
+apply: (mx_abs_irr_cent_scalar absG).
 by apply/centgmxP=> y Gy; rewrite -!repr_mxM // (centsP cGG).
 Qed.
 
@@ -3442,7 +3442,7 @@ rewrite inE -val_eqE /= PackSocleK eq_sym.
 by apply/component_mx_isoP; rewrite ?subgK //; apply: Clifford_iso.
 Qed.
 
-Lemma Clifford_astab1 (W : sH) : 'C[W | 'Cl] = rstabs rG W. 
+Lemma Clifford_astab1 (W : sH) : 'C[W | 'Cl] = rstabs rG W.
 Proof.
 apply/setP=> x; rewrite !inE; apply: andb_id2l => Gx.
 rewrite sub1set inE (sameP eqP socleP) !val_Clifford_act //.
@@ -3638,7 +3638,7 @@ have UvalI: (valI <= U)%MS.
 exists (valI *m in_factmod _ 1%:M *m in_submod _ 1%:M) => [||x Gx].
 - apply: (@addIn (\rank (U :&: V) + \rank V)%N); rewrite genmxE addnA addnCA.
   rewrite /nI genmxE !{1}mxrank_in_factmod 2?(addsmx_idPr _) //.
-  by rewrite -mxrank_sum_cap addnC. 
+  by rewrite -mxrank_sum_cap addnC.
 - rewrite -kermx_eq0; apply/rowV0P=> u; rewrite (sameP sub_kermxP eqP).
   rewrite mulmxA -in_submodE mulmxA -in_factmodE -(inj_eq val_submod_inj).
   rewrite linear0 in_submodK ?in_factmod_eq0 => [Vvu|]; last first.
@@ -4329,7 +4329,7 @@ rewrite -ker_irr_comp_op sub_capmx (sameP sub_kermxP eqP) mul_vec_lin.
 by rewrite 2!linearB /= eqAB subrr linear0 addmx_sub ?eqmx_opp /=.
 Qed.
 
-Lemma rank_irr_comp : \rank 'R_iG = \rank E_G. 
+Lemma rank_irr_comp : \rank 'R_iG = \rank E_G.
 Proof.
 symmetry; rewrite -{1}irr_comp_envelop; apply/mxrank_injP.
 by rewrite ker_irr_comp_op.
@@ -4544,7 +4544,7 @@ have [_ nG'G] := andP (der_normal 1 G); apply/eqP; rewrite -card_quotient //.
 have cGqGq: abelian (G / G^`(1))%g by apply: sub_der1_abelian.
 have F'Gq: [char F]^'.-group (G / G^`(1))%g by apply: morphim_pgroup.
 have splitGq: group_splitting_field (G / G^`(1))%G.
-  exact: quotient_splitting_field. 
+  exact: quotient_splitting_field.
 rewrite -(sum_irr_degree sGq) // -sum1_card.
 pose rG (j : sGq) := morphim_repr (socle_repr j) nG'G.
 have irrG j: mx_irreducible (rG j) by apply/morphim_mx_irr; apply: socle_irr.
@@ -4785,7 +4785,7 @@ suffices defU: (\sum_i oapp W_ V i :=: U)%MS.
 apply: eqmx_trans defVW; rewrite (bigD1 None) //=; apply/eqmxP.
 have [i0 _ | I0] := pickP I.
   by rewrite (reindex some) ?addsmxS ?defW //; exists (odflt i0) => //; case.
-rewrite big_pred0 //; last by case => // /I0.
+rewrite big_pred0 //; last by case=> // /I0.
 by rewrite !addsmxS ?sub0mx // -defW big_pred0.
 Qed.
 
@@ -4841,7 +4841,7 @@ have sVS: (V <= \sum_(W : sG | has (fun Mi => Mi <= W) Ms) W)%MS.
   rewrite [V](big_nth 0) big_mkord; apply/sumsmx_subP=> i _.
   set Mi := Ms`_i; have MsMi: Mi \in Ms by apply: mem_nth.
   have simMi := simMs _ MsMi; have S_Mi := component_socle sG simMi.
-  rewrite (sumsmx_sup (PackSocle S_Mi)) ?PackSocleK //. 
+  rewrite (sumsmx_sup (PackSocle S_Mi)) ?PackSocleK //.
   by apply/hasP; exists Mi; rewrite ?component_mx_id.
 have [W MsW isoWM] := subSocle_iso simM (submx_trans sMV sVS).
 have [Mi MsMi sMiW] := hasP MsW; apply/hasP; exists Mi => //.
@@ -4908,7 +4908,7 @@ Lemma map_mx_faithful : mx_faithful rGf = mx_faithful rG.
 Proof. by rewrite /mx_faithful rker_map. Qed.
 
 Lemma map_mx_abs_irr :
-  mx_absolutely_irreducible rGf = mx_absolutely_irreducible rG. 
+  mx_absolutely_irreducible rGf = mx_absolutely_irreducible rG.
 Proof.
 by rewrite /mx_absolutely_irreducible -map_enveloping_algebra_mx row_full_map.
 Qed.
@@ -5284,7 +5284,7 @@ rewrite {1}mulSn -Bfree -{1}rBj {rBj} -mxrank_disjoint_sum.
   rewrite mxrankS // addsmx_sub -[m.+1]/(1 + m)%N; apply/andP; split.
     apply/row_subP=> k; rewrite row_mul mul_rV_lin1 /=.
     apply: eq_row_sub (mxvec_index (lshift _ 0) k)  _.
-    by rewrite !rowK mxvecK mxvecE mxE row_mxEl mxE -row_mul mul1mx. 
+    by rewrite !rowK mxvecK mxvecE mxE row_mxEl mxE -row_mul mul1mx.
   apply/row_subP; case/mxvec_indexP=> i k.
   apply: eq_row_sub (mxvec_index (rshift 1 i) k) _.
   by rewrite !rowK !mxvecE 2!mxE row_mxEr.
diff --git a/mathcomp/character/vcharacter.v b/mathcomp/character/vcharacter.v
index 5b1ff05..97ad828 100644
--- a/mathcomp/character/vcharacter.v
+++ b/mathcomp/character/vcharacter.v
@@ -248,7 +248,7 @@ by rewrite !cfunE rpredB // rpred_Cnat ?Cnat_char1.
 Qed.
 
 Lemma Cint_cfdot_vchar_irr i phi : phi \in 'Z[irr G] -> '[phi, 'chi_i] \in Cint.
-Proof.  
+Proof.
 case/vcharP=> chi1 Nchi1 [chi2 Nchi2 ->].
 by rewrite cfdotBl rpredB // rpred_Cnat ?Cnat_cfdot_char_irr.
 Qed.
@@ -310,7 +310,7 @@ have notSnu0: 0 \notin map nu S.
   apply: contra notS0 => /mapP[phi Sphi /esym/eqP].
   by rewrite -cfnorm_eq0 Inu ?Z_S // cfnorm_eq0 => /eqP <-.
 apply/pairwise_orthogonalP; split; first by rewrite /= notSnu0 map_inj_in_uniq.
-move=>_ _ /mapP[phi Sphi ->] /mapP[psi Spsi ->].
+move=> _ _ /mapP[phi Sphi ->] /mapP[psi Spsi ->].
 by rewrite (inj_in_eq inj_nu) // Inu ?Z_S //; apply: dotSS.
 Qed.
 
@@ -553,9 +553,9 @@ Lemma isometry_in_zchar nu : {in S &, isometry nu} -> {in 'Z[S] &, isometry nu}.
 Proof.
 move=> Inu _ _ /zchar_nth_expansion[u Zu ->] /zchar_nth_expansion[v Zv ->].
 rewrite !raddf_sum; apply: eq_bigr => j _ /=.
-rewrite !cfdot_suml; apply: eq_bigr => i _.  
+rewrite !cfdot_suml; apply: eq_bigr => i _.
 by rewrite !raddfZ_Cint //= !cfdotZl !cfdotZr Inu ?mem_nth.
-Qed. 
+Qed.
 
 End Isometries.
 
@@ -702,7 +702,7 @@ have [j def_chi_j]: {j | 'chi_j = phi}.
 exists j; rewrite ?cfkerEirr def_chi_j //; apply/subsetP => x /setDP[Gx notHx].
 rewrite inE cfunE def_phi // cfunE -/a cfun1E // Gx mulr1 cfIndE //.
 rewrite big1 ?mulr0 ?add0r // => y Gy; apply/theta0/(contra _ notHx) => Hxy.
-by rewrite -(conjgK y x) cover_imset -class_supportEr mem_imset2 ?groupV. 
+by rewrite -(conjgK y x) cover_imset -class_supportEr mem_imset2 ?groupV.
 Qed.
 
 End MoreVchar.
@@ -732,7 +732,7 @@ Proof. by rewrite !inE mem_irr. Qed.
 Lemma dirrP f :
   reflect (exists b : bool, exists i, f = (-1) ^+ b *: 'chi_i) (f \in dirr G).
 Proof.
-apply: (iffP idP) => [| [b [i ->]]]; last by rewrite dirr_sign irr_dirr. 
+apply: (iffP idP) => [| [b [i ->]]]; last by rewrite dirr_sign irr_dirr.
 case/orP=> /irrP[i Hf]; first by exists false, i; rewrite scale1r.
 by exists true, i; rewrite scaleN1r -Hf opprK.
 Qed.