Adapt to https://github.com/coq/coq/pull/18031

theories/BGappendixC.v

@@ -31,7 +31,7 @@ Let nU := ((p ^ q).-1 %/ p.-1)%N.
 (* External statement of the finite field assumption. *)
 Variant finFieldImage : Prop :=
   FinFieldImage (F : finFieldType) (sigma : {morphism P >-> F}) of
-     isom P [set: F] sigma & sigma @*^-1 <[1 : F]> = P0
+     isom P [set: F] sigma & sigma @*^-1 <[1%R : F]> = P0
    & exists2 sigmaU : {morphism U >-> {unit F}},
      'injm sigmaU & {in P & U, morph_act 'J 'U sigma sigmaU}.
 

theories/PFsection1.v

@@ -35,7 +35,7 @@
 Lemma odd_eq_conj_irr1 (G : {group gT}) t :
   odd #|G| -> (('chi[G]_t)^*%CF == 'chi_t) = ('chi_t == 1).
 Proof.
-rewrite -coprimen2 => oddG; pose A := <[1 : 'Z_2]>.
+rewrite -coprimen2 => oddG; pose A := <[1%R : 'Z_2]>.
 have Z2P (a : 'Z_2): a = 0 \/ a = 1 by apply/pred2P; case: a => -[|[]].
 pose Ito (t : Iirr G) := [fun a : 'Z_2 => iter a (@conjC_Iirr _ G) t].
 pose Cto (C : {set gT}) := [fun a : 'Z_2 => iter a invg C].
@@ -163,7 +163,7 @@
 case: (i =P k) => // eq_ik; exists (j, i, j', true).
 rewrite !scaler_sign !opprB /= !inE eq_sym negb_or neq_ij neq_jj'.
 by rewrite eq_ik neq_kj'.
 Qed.
 
 Let vchar_isometry_base4 (eps : bool) i j k n m :
     let f1 := 'chi_j - 'chi_i in
@@ -177,11 +177,11 @@
   by apply: IH; rewrite // -opprB cfdotNl (nm_ji, nm_ki) opprK.
 rewrite !cfdotBl !cfdotBr !cfdot_irr !opprB addrAC addrA.
 do 2!move/(canRL (subrK _)); rewrite -(natrD _ 1) -!natrD.
 move/(can_inj natCK); case: (m == i) => //.
 case: eqP => // ->; case: (j == i) => // _.
 rewrite subr0 add0r => /(canRL (subrK _)); rewrite -(natrD _ 1).
 by move/(can_inj natCK); rewrite (negbTE Hjk).
 Qed.
 
 (* This is Peterfalvi (1.4). *)
 Lemma vchar_isometry_base m L (Chi : m.-tuple 'CF(H)) 
@@ -450,11 +450,11 @@
 
 Hypothesis nsHG: H <| G.
 (* begin hide *)
 Let sHG : H \subset G. Proof. exact: normal_sub. Qed.
 Let nHG : G \subset 'N(H). Proof. exact: normal_norm. Qed.
 Let nsHT : H <| T. Proof. exact: normal_Inertia. Qed.
 Let sHT : H \subset T. Proof. exact: normal_sub. Qed.
 Let nHT : T \subset 'N(H). Proof. exact: normal_norm. Qed.
 Let sTG : T \subset G. Proof. exact: subsetIl. Qed.
 (* end hide *)
 
@@ -476,7 +476,7 @@
 
 (* This is Peterfalvi (1.7)(b). *)
 Lemma cfInd_central_Inertia :
    exists2 e, [/\ e \in Cnat, e != 0 & {in calA, forall t, e_ t = e}]
            & [/\ 'Ind[G] theta = e *: \sum_(j in calB) 'chi_j,
                  #|calB|%:R = #|T : H|%:R / e ^+ 2
                & {in calB, forall i, 'chi_i 1%g = #|G : T|%:R * e * theta 1%g}].
@@ -484,11 +484,11 @@
 have [t1 At1] := constt_cfInd_irr s sHT; pose psi1 := 'chi_t1.
 pose e := '['Ind theta, psi1].
 have NthT: 'Ind[T] theta \is a character by rewrite cfInd_char ?irr_char.
 have Ne: e \in Cnat by rewrite Cnat_cfdot_char_irr.
 have Dpsi1H: 'Res[H] psi1 = e *: theta.
   have psi1Hs: s \in irr_constt ('Res psi1) by rewrite -constt_Ind_Res.
   rewrite (Clifford_Res_sum_cfclass nsHT psi1Hs) cfclass_invariant ?subsetIr //.
   by rewrite big_seq1 cfdot_Res_l cfdotC conj_Cnat.
 have linL j: 'chi[T / H]_j \is a linear_char by apply/char_abelianP.
 have linLH j: ('chi_j %% H)%CF \is a linear_char := cfMod_lin_char (linL j).
 pose LtoT (j : Iirr (T / H)) := mul_mod_Iirr t1 j.
@@ -541,7 +541,7 @@
 have solT: solvable (T / H) := abelian_sol abTbar.
 have [|t []] := extend_solvable_coprime_irr nsHT solT ITtheta; last by exists t.
 rewrite coprime_sym coprimeMl !(coprime_dvdl _ hallH) ?cfDet_order_dvdG //.
 by rewrite -dvdC_nat !CdivE truncCK ?Cnat_irr1 // dvd_irr1_cardG.
 Qed.
 
 End IndSumInertia.