move odd_order to its own repository

1 files changed, 0 insertions, 762 deletions

diff --git a/mathcomp/odd_order/PFsection1.v b/mathcomp/odd_order/PFsection1.v
deleted file mode 100644
index 8e0b539..0000000
--- a/mathcomp/odd_order/PFsection1.v
+++ /dev/null
@@ -1,762 +0,0 @@
-(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
-(* Distributed under the terms of CeCILL-B.                                  *)
-Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp
-Require Import ssrbool ssrfun eqtype ssrnat seq path div choice.
-From mathcomp
-Require Import fintype tuple finfun bigop prime ssralg finset fingroup morphism.
-From mathcomp
-Require Import perm automorphism quotient action zmodp finalg center commutator.
-From mathcomp
-Require Import poly cyclic pgroup nilpotent matrix mxalgebra mxrepresentation.
-From mathcomp
-Require Import vector falgebra fieldext ssrnum algC rat algnum galois.
-From mathcomp
-Require Import classfun character inertia integral_char vcharacter.
-From mathcomp
-Require ssrint.
-
-(******************************************************************************)
-(* This file covers Peterfalvi, Section 1: Preliminary results.               *)
-(******************************************************************************)
-
-Set Implicit Arguments.
-Unset Strict Implicit.
-Unset Printing Implicit Defensive.
-
-Import GroupScope GRing.Theory Num.Theory.
-Local Open Scope ring_scope.
-
-Local Notation algCF := [fieldType of algC].
-
-Section Main.
-
-Variable gT : finGroupType.
-
-(* This is Peterfalvi (1.1). *)
-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]>.
-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].
-have IactP: is_action A Ito.
-  split=> [|i /Z2P[]->] /Z2P[]-> //=; last by rewrite conjC_IirrK.
-  exact/inv_inj/conjC_IirrK.
-have CactP: is_action A Cto.
-  by split=> [|C /Z2P[]->] /Z2P[]-> //=; [apply: invg_inj | rewrite invgK].
-pose Iact := Action IactP; pose Cact := Action CactP.
-have n_cG_A: [acts A, on classes G | Cact].
-  rewrite cycle_subG !inE cycle_id; apply/subsetP=> _ /imsetP[x Gx ->].
-  by rewrite !inE /= -classVg mem_classes ?groupV.
-transitivity (t \in [set 0]); last by rewrite inE irr_eq1.
-suffices{t} /eqP->: [set 0] == 'Fix_Iact[1].
-  by rewrite !inE sub1set inE -(inj_eq irr_inj) conjC_IirrE.
-rewrite eqEcard !(sub1set, inE) conjC_Iirr_eq0 eqxx /=.
-rewrite (card_afix_irr_classes (cycle_id _) n_cG_A) => [|i x xy Gx]; last first.
-  rewrite inE => {xy}/imsetP[y Gy /(canRL invgK)->].
-  by rewrite -conjVg cfunJ {y Gy}//= conjC_IirrE cfunE -irr_inv invgK.
-have ->: #|[set 0 : Iirr G]| = #|[1 {set gT}]| by rewrite !cards1.
-apply/subset_leq_card/subsetP=> _ /setIdP[/imsetP[x Gx ->] /afix1P-DxGV].
-have /imsetP[y Gy DxV]: x^-1%g \in x ^: G by rewrite -DxGV memV_invg class_refl.
-have{Gy} cxy: y \in 'C[x].
-  suffices cxy2: (y ^+ 2)%g \in 'C[x] by rewrite -(expgK oddG Gy) groupX.
-  by rewrite cent1C cent1E conjgC conjgM -DxV conjVg -DxV invgK.
-rewrite inE classG_eq1 -in_set1 -(expgK oddG Gx) groupX // inE.
-by rewrite -eq_invg_mul DxV conjgE -(cent1P cxy) mulKg.
-Qed.
-
-Variables G H : {group gT}.
-
-(* This is Peterfalvi (1.2). *)
-Lemma irr_reg_off_ker_0 t g : g \in G ->
-  H <| G -> ~~ (H \subset cfker 'chi[G]_t) -> 'C_H[g] = 1%g -> 'chi_t g = 0.
-Proof.
-pose kerH i := H \subset cfker 'chi[G]_i => Gg nsHG kerH't regHg; apply/eqP.
-pose sum_norm2 x := \sum_i `|'chi_i x| ^+ 2.
-have norm2_ge0 a: 0 <= `|a| ^+ 2 :> algC by rewrite exprn_ge0 ?normr_ge0.
-have{regHg}: sum_norm2 gT G g <= sum_norm2 _ (G / H)%G (coset H g).
-  rewrite ![sum_norm2 _ _ _](eq_bigr _ (fun _ _ => normCK _)).
-  rewrite !second_orthogonality_relation ?mem_quotient // !class_refl ler_nat.
-  suffices /card_isog->: 'C_G[g] \isog 'C_G[g] / H.
-    exact/subset_leq_card/quotient_subcent1.
-  by apply/quotient_isog; rewrite ?subIset 1?normal_norm // setICA regHg setIg1.
-rewrite /sum_norm2 (bigID kerH) ?sum_norm_irr_quo //= -ler_subr_addl subrr.
-rewrite ler_eqVlt psumr_eq0 ?ler_gtF ?sumr_ge0 // orbF => /allP/(_ t)/implyP.
-by rewrite mem_index_enum kerH't expf_eq0 normr_eq0.
-Qed.
-
-(* This is Peterfalvi (1.3)(a). *)
-Lemma equiv_restrict_compl A m (Phi : m.-tuple 'CF(H)) (mu : 'CF(G)) d :
-    H \subset G -> A <| H -> basis_of 'CF(H, A) Phi ->
-  ({in A, mu =1 \sum_i d i *: 'chi_i} <-> 
-    (forall j : 'I_m,
-        \sum_i '[Phi`_j, 'chi_i] * (d i)^* = '['Ind[G] Phi`_j, mu])).
-Proof.
-move=> sHG nsAH BPhi; have [sAH nAH] := andP nsAH.
-have APhi (i : 'I_m) : Phi`_i \in 'CF(H, A).
-  by apply: (basis_mem BPhi _); apply: mem_nth; rewrite size_tuple.
-pose D := 'Res[H] mu - \sum_i d i *: 'chi_i.
-transitivity (D \in 'CF(H, H :\: A)).
-  split=> [A'D | /cfun_onP A'D x Ax].
-    apply/cfun_onP=> x; rewrite inE negb_and negbK.
-    case/orP=> [Ax | /cfun0-> //]; rewrite !cfunE -A'D //.
-    by rewrite cfResE ?subrr ?(subsetP sAH).
-  have:= A'D x; rewrite !cfunE !inE Ax => /(_ isT)/(canRL (subrK _)).
-  by rewrite add0r cfResE // ?(subsetP sAH).
-have F0 (j : 'I_m) : 
-   (\sum_i '[Phi`_j, 'chi_i] * (d i)^* == '['Ind Phi`_j, mu])
-      = ('[Phi`_j, D] == 0).
-  rewrite raddfB raddf_sum /= Frobenius_reciprocity subr_eq0 eq_sym.
-  by congr (_ == _); apply: eq_bigr=> i _; rewrite cfdotZr mulrC.
-split=> [HH j | HH].
-  by apply/eqP; rewrite F0; apply/eqP; apply: cfdot_complement.
-have{F0} F1 (j : 'I_m) : '[Phi`_j, D]_H = 0.
-  by have/eqP := HH j; rewrite F0 => /eqP.
-have: (D \in 'CF(H))%VS by rewrite memvf.
-rewrite -(cfun_complement nsAH) => /memv_addP[f Cf [g Cg defD]].
-have: '[f, f + g] = 0.
-  rewrite -defD (coord_basis BPhi Cf) cfdot_suml.
-  by rewrite big1 // => i _; rewrite cfdotZl F1 mulr0.
-rewrite raddfD /= {1}(cfdot_complement Cf Cg) addr0 => /eqP.
-by rewrite cfnorm_eq0 defD => /eqP->; rewrite add0r.
-Qed.
-
-(* This is Peterfalvi (1.3)(b). *)
-Lemma equiv_restrict_compl_ortho A m (Phi : m.-tuple 'CF(H)) mu_ :
-    H \subset G -> A <| H -> basis_of 'CF(H, A) Phi -> 
-     (forall i j, '[mu_ i, mu_ j] = (i == j)%:R) ->
-     (forall j : 'I_m, 'Ind[G] Phi`_j = \sum_i '[Phi`_j, 'chi_i] *: mu_ i) ->
-   [/\ forall i, {in A, mu_ i =1 'chi_i}
-     & forall mu, (forall i, '[mu, mu_ i] = 0) -> {in A, forall x, mu x = 0}].
-Proof.
-move=> HsG nsAH /equiv_restrict_compl Phi_A Mo IP; split=> [/= i | mu Cmu x Ax].
-  have->: 'chi[H]_i = \sum_j (j == i)%:R *: 'chi_j.
-    rewrite (bigD1 i) //= eqxx scale1r big1 ?addr0 // => j /negPf->.
-    by rewrite scale0r.
-  apply/Phi_A=> // j; rewrite IP cfdot_suml.
-  by apply: eq_bigr=> k _; rewrite cfdotZl rmorph_nat Mo.
-transitivity ((\sum_j 0 *: 'chi[H]_j) x); last first.
-  by rewrite sum_cfunE big1 // => j _; rewrite cfunE mul0r.
-move: x Ax; apply/Phi_A=> // j.
-rewrite -mulr_suml rmorph0 mulr0 IP cfdot_suml big1 // => k _.
-by rewrite cfdotZl [d in _ * d]cfdotC Cmu rmorph0 mulr0.
-Qed.
-
-Let vchar_isometry_base3 f f' : 
-  f \in 'Z[irr G, G^#] -> '[f]_G = 2%:R ->
-  f' \in 'Z[irr G, G^#] -> '[f']_G = 2%:R ->
-  '[f, f'] = 1 ->
-   exists es : _ * bool, let: (i, j, k, epsilon) := es in
-     [/\  f = (-1) ^+ epsilon *: ('chi_j - 'chi_i),
-          f' = (-1) ^+ epsilon *: ('chi_j - 'chi_k)
-        & uniq [:: i; j; k]].
-Proof.
-move=> Hf H2f Hf1 H2f1.
-have [j [i neq_ij ->]] := vchar_norm2 Hf H2f.
-have [j' [k neq_kj' ->]] := vchar_norm2 Hf1 H2f1.
-rewrite cfdotBl !cfdotBr !cfdot_irr opprB addrAC !addrA.
-do 2!move/(canRL (subrK _)); rewrite -(natrD _ 1) -!natrD => /eqP.
-rewrite eqr_nat; have [eq_jj' | neq_jj'] := altP (j =P j').
-  rewrite (eq_sym j) -eq_jj' {1}eq_jj' (negbTE neq_ij) (negbTE neq_kj').
-  rewrite eqSS (can_eq oddb) => /eqP neq_ik; exists (i, j, k, false).
-  by rewrite !scaler_sign /= !inE neq_ik orbF neq_ij eq_sym eq_jj' neq_kj'.
-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
-    let f2 := 'chi_k - 'chi_i in
-    let f3 := 'chi_n - 'chi_m in
-    j != k -> '[f3, f1]_G = (-1) ^+ eps -> '[f3, f2] = (-1) ^+ eps -> 
-  if eps then n == i else m == i.
-Proof.
-move=> /= Hjk; wlog ->: eps n m / eps = false.
-  case: eps; last exact; move/(_ false m n)=> IH nm_ji nm_ki.
-  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)) 
-                            (tau : {linear 'CF(H) -> 'CF(G)}) :
-    (1 < m)%N -> {subset Chi <= irr H} -> free Chi ->
-    (forall chi, chi \in Chi -> chi 1%g = Chi`_0 1%g) ->
-    (forall i : 'I_m, (Chi`_i - Chi`_0) \in 'CF(H, L)) ->
-    {in 'Z[Chi, L], isometry tau, to 'Z[irr G, G^#]} ->
-    exists2 mu : m.-tuple (Iirr G),
-      uniq mu
-    & exists epsilon : bool, forall i : 'I_m,
-      tau (Chi`_i - Chi`_0) = (-1) ^+ epsilon *: ('chi_(mu`_i) - 'chi_(mu`_0)).
-Proof.
-case: m Chi => [|[|m]] // Chi _ irrChi Chifree Chi1 ChiCF [iso_tau Ztau].
-rewrite -(tnth_nth 0 _ 0); set chi := tnth Chi.
-have chiE i: chi i = Chi`_i by rewrite -tnth_nth.
-have inChi i: chi i \in Chi by apply: mem_tnth.
-have{irrChi} irrChi i: chi i \in irr H by apply: irrChi.
-have eq_chi i j: (chi i == chi j) = (i == j).
-  by rewrite /chi !(tnth_nth 0) nth_uniq ?size_tuple ?free_uniq.
-have dot_chi i j: '[chi i, chi j] = (i == j)%:R.
-  rewrite -eq_chi; have [/irrP[{i}i ->] /irrP[{j}j ->]] := (irrChi i,irrChi j).
-  by rewrite cfdot_irr inj_eq //; apply: irr_inj.
-pose F i j := chi i - chi j.
-have DF i j : F i j =  F i 0 - F j 0 by rewrite /F opprB addrA subrK.
-have ZF i j: F i j \in 'Z[Chi, L].
-  by rewrite zchar_split rpredB ?mem_zchar // DF memvB // /F !chiE.
-have htau2 i j: i != j -> '[tau (F i j)] = 2%:R.
-  rewrite iso_tau // cfnormB -cfdotC !dot_chi !eqxx eq_sym => /negbTE->.
-  by rewrite -!natrD subr0.
-have htau1 i j: j != 0 -> j != i -> i != 0 -> '[tau (F i 0), tau (F j 0)] = 1.
-  rewrite iso_tau // cfdotBl !cfdotBr opprB !dot_chi !(eq_sym j).
-  by do 3!move/negbTE->; rewrite !subr0 add0r.
-have [m0 | nz_m] := boolP (m == 0%N).
-  rewrite -2!eqSS eq_sym in m0; move: (htau2 1 0 isT).
-  case/(vchar_norm2 (Ztau _ (ZF 1 0))) => [k1 [k0 neq_k01 eq_mu]].
-  pose mu := @Tuple _ _ [:: k0; k1] m0.
-  exists mu; first by rewrite /= andbT inE.
-  exists false => i; rewrite scale1r chiE.
-  have: (i : nat) \in iota 0 2 by rewrite mem_iota (eqP m0) (valP i).
-  rewrite !inE; case/pred2P=> ->; first by rewrite !subrr linear0.
-  by rewrite -eq_mu /F !chiE.
-have m_gt2: (2 < m.+2)%N by rewrite !ltnS lt0n.
-pose i2 := Ordinal m_gt2.
-case: (@vchar_isometry_base3 (tau (F 1 0)) (tau (F i2 0))); auto.
-case=> [[[k1 k0] k2] e] []; set d := (-1) ^+ e => eq10 eq20.
-rewrite /= !inE => /and3P[/norP[nek10 nek12]]; rewrite eq_sym => nek20 _.
-have muP i:
-  {k | (i == 0) ==> (k == k0) & tau (F i 0) == d *: ('chi_k0 - 'chi_k)}.
-- apply: sig2W; have [-> | nei0] := altP (i =P 0).
-    by exists k0; rewrite ?eqxx // /F !subrr !linear0.
-  have /(vchar_norm2 (Ztau _ (ZF i 0)))[k [k' nekk' eqFkk']] := htau2 i 0 nei0.
-  have [-> | neq_i1] := eqVneq i 1; first by exists k1; rewrite // -eq10.
-  have [-> | neq_i2] := eqVneq i i2; first by exists k2; rewrite // -eq20.
-  have:= @vchar_isometry_base4 (~~ e) k0 k1 k2 k k' nek12.
-  have ZdK u v w: '[u, v - w]_G = (-1) ^+ (~~ e) * '[u, d *: (w - v)].
-    rewrite cfdotZr rmorph_sign mulrA -signr_addb addNb addbb mulN1r.
-    by rewrite -cfdotNr opprB.
-  rewrite -eqFkk' ZdK -eq10 {}ZdK -eq20 !htau1 //; try by rewrite eq_sym.
-  move/(_ (mulr1 _) (mulr1 _)); rewrite /d eqFkk'.
-  by case e => /eqP <-; [exists k | exists k']; rewrite ?scaler_sign ?opprB.
-pose mu := [tuple of [seq s2val (muP i) | i <- ord_tuple m.+2]]; exists mu.
-  rewrite map_inj_uniq ?enum_uniq // => i j.
-  case: (muP i) (muP j) => /= ki _ /eqP eq_i0 [/= kj _ /eqP eq_j0] eq_kij.
-  apply/eqP; rewrite -eq_chi -subr_eq0 -cfnorm_eq0 -iso_tau ?ZF //.
-  rewrite -[chi i](subrK (chi 0)) -addrA linearD eq_i0 eq_kij -eq_j0.
-  by rewrite -linearD -opprB subrr !raddf0.
-exists (~~ e) => i; rewrite -addbT signr_addb -/d -scalerA scaleN1r opprB.
-rewrite -!tnth_nth -/(F i 0) tnth_map tnth_ord_tuple.
-suffices /= ->: mu`_0 = k0 by case: (muP i) => /= k _ /eqP.
-rewrite -(tnth_nth 0 _ 0) tnth_map tnth_ord_tuple.
-by case: (muP 0) => /= k /(k =P k0).
-Qed.
-
-(* This is Peterfalvi (1.5)(a). *)
-Lemma cfResInd_sum_cfclass t : H <| G ->
-  'Res[H] ('Ind[G] 'chi_t)
-     = #|'I_G['chi_t] : H|%:R *: \sum_(xi <- ('chi_t ^: G)%CF) xi.
-Proof.
-set T := 'I_G['chi_t] => nsHG; have [sHG nHG] := andP nsHG.
-apply/cfun_inP=> h Hh; rewrite cfResE ?cfIndE // cfunE sum_cfunE.
-apply: (canLR (mulKf (neq0CG H))).
-rewrite mulrA -natrM Lagrange ?sub_Inertia //= -/T reindex_cfclass //=.
-rewrite mulr_sumr [s in _ = s]big_mkcond /= (reindex_inj invg_inj).
-rewrite (partition_big (conjg_Iirr t) xpredT) //=; apply: eq_bigr => i _.
-have [[y Gy chi_i] | not_i_t] := cfclassP _ _ _; last first.
-  apply: big1 => z; rewrite groupV => /andP[Gz /eqP def_i].
-  by case: not_i_t; exists z; rewrite // -def_i conjg_IirrE.
-rewrite -(card_rcoset _ y) mulr_natl -sumr_const; apply: eq_big => z.
-  rewrite -(inj_eq irr_inj) conjg_IirrE chi_i mem_rcoset inE groupMr ?groupV //.
-  apply: andb_id2l => Gz; rewrite eq_sym (cfConjg_eqE _ nsHG) //.
-  by rewrite mem_rcoset inE groupM ?groupV.
-rewrite groupV => /andP[Gz /eqP <-].
-by rewrite conjg_IirrE cfConjgE ?(subsetP nHG).
-Qed.
-
-(* This is Peterfalvi (1.5)(b), main formula. *)
-Lemma cfnorm_Ind_irr t :
-  H <| G -> '['Ind[G] 'chi[H]_t] = #|'I_G['chi_t] : H|%:R.
-Proof.
-set r := _%:R => HnG; have HsG := normal_sub HnG.
-rewrite -Frobenius_reciprocity cfResInd_sum_cfclass //= cfdotZr rmorph_nat -/r.
-rewrite reindex_cfclass // cfdot_sumr (bigD1 t) ?cfclass_refl //= cfnorm_irr.
-rewrite big1 ?addr0 ?mulr1 // => j /andP[_ /negbTE].
-by rewrite eq_sym cfdot_irr => ->.
-Qed.
-
-(* This is Peterfalvi (1.5)(b), irreducibility remark. *)
-Lemma inertia_Ind_irr t :
-  H <| G -> 'I_G['chi[H]_t] \subset H -> 'Ind[G] 'chi_t \in irr G.
-Proof.
-rewrite -indexg_eq1 => nsHG /eqP r1.
-by rewrite irrEchar cfInd_char ?irr_char //= cfnorm_Ind_irr ?r1.
-Qed.
-
-(* This is Peterfalvi (1.5)(c). *)
-Lemma cfclass_Ind_cases t1 t2 : H <| G ->
-   if 'chi_t2 \in ('chi[H]_t1 ^: G)%CF
-   then 'Ind[G] 'chi_t1 = 'Ind[G] 'chi_t2 
-   else '['Ind[G] 'chi_t1, 'Ind[G] 'chi_t2] = 0.
-Proof.
-move=> nsHG; have [/cfclass_Ind-> // | not_ch1Gt2] := ifPn.
-rewrite -Frobenius_reciprocity cfResInd_sum_cfclass // cfdotZr rmorph_nat.
-rewrite cfdot_sumr reindex_cfclass // big1 ?mulr0 // => j; rewrite cfdot_irr.
-case: eqP => // <- /idPn[]; apply: contra not_ch1Gt2 => /cfclassP[y Gy ->].
-by apply/cfclassP; exists y^-1%g; rewrite ?groupV ?cfConjgK.
-Qed.
-
-(* Useful consequences of (1.5)(c) *)
-Lemma not_cfclass_Ind_ortho i j :
-    H <| G -> ('chi_i \notin 'chi_j ^: G)%CF ->
-  '['Ind[G, H] 'chi_i, 'Ind[G, H] 'chi_j] = 0.
-Proof. by move/(cfclass_Ind_cases i j); rewrite cfclass_sym; case: ifP. Qed.
-
-Lemma cfclass_Ind_irrP i j :
-    H <| G ->
-  reflect ('Ind[G, H] 'chi_i = 'Ind[G, H] 'chi_j) ('chi_i \in 'chi_j ^: G)%CF.
-Proof.
-move=> nsHG; have [sHG _] := andP nsHG.
-case: ifP (cfclass_Ind_cases j i nsHG) => [|_ Oji]; first by left.
-right=> eq_chijG; have /negP[]: 'Ind[G] 'chi_i != 0 by apply: Ind_irr_neq0.
-by rewrite -cfnorm_eq0 {1}eq_chijG Oji.
-Qed.
-
-Lemma card_imset_Ind_irr (calX : {set Iirr H}) :
-    H <| G -> {in calX, forall i, 'Ind 'chi_i \in irr G} ->
-    {in calX & G, forall i y, conjg_Iirr i y \in calX} ->
-  #|calX| = (#|G : H| * #|[set cfIirr ('Ind[G] 'chi_i) | i in calX]|)%N.
-Proof.
-move=> nsHG irrIndX sXGX; have [sHG _] := andP nsHG; set f := fun i => cfIirr _.
-rewrite -sum1_card (partition_big_imset f) /= mulnC -sum_nat_const.
-apply: eq_bigr => _ /imsetP[i Xi ->]; transitivity (size (cfclass 'chi_i G)).
-  rewrite -sum1_size reindex_cfclass //; apply: eq_bigl => j.
-  case Xj: (j \in calX).
-    rewrite -(inj_eq irr_inj) !(cfIirrPE irrIndX) //.
-    exact/eqP/cfclass_Ind_irrP.
-  apply/esym/(contraFF _ Xj)=> /cfclassP[y Gy Dj].
-  by rewrite -conjg_IirrE in Dj; rewrite (irr_inj Dj) sXGX.
-rewrite -(Lagrange_index (Inertia_sub G 'chi_i)) ?sub_Inertia //.
-rewrite -size_cfclass ((#|_ : _| =P 1)%N _) ?muln1 // -eqC_nat.
-by rewrite -cfnorm_Ind_irr // -(cfIirrPE irrIndX) ?cfnorm_irr.
-Qed.
-
-(* This is Peterfalvi (1.5)(d). *)
-Lemma scaled_cfResInd_sum_cfclass t : H <| G ->
-  let chiG := 'Ind[G] 'chi_t in
-  (chiG 1%g / '[chiG]) *: 'Res[H] chiG
-     = #|G : H|%:R *: (\sum_(xi <- ('chi_t ^: G)%CF) xi 1%g *: xi).
-Proof.
-move=> nsHG chiG; have [sHG _] := andP nsHG.
-rewrite cfResInd_sum_cfclass // cfnorm_Ind_irr // scalerA cfInd1 //.
-rewrite divfK ?pnatr_eq0 -?lt0n // -scalerA linear_sum !reindex_cfclass //=.
-congr (_ *: _); apply: eq_bigr => _ /cfclassP[y _ ->].
-by rewrite cfConjg1.
-Qed.
-
-(* This is Peterfalvi (1.5)(e). *)
-Lemma odd_induced_orthogonal t :
-     H <| G -> odd #|G| -> t != 0 ->
-  '['Ind[G, H] 'chi_t, ('Ind[G] 'chi_t)^*] = 0.
-Proof.
-move=> nsHG oddG nz_t; have [sHG _] := andP nsHG.
-have:= cfclass_Ind_cases t (conjC_Iirr t) nsHG.
-rewrite conjC_IirrE conj_cfInd; case: cfclassP => // [[g Gg id_cht]].
-have oddH: odd #|H| := pgroup.oddSg sHG oddG.
-case/eqP: nz_t; apply: irr_inj; rewrite irr0.
-apply/eqP; rewrite -odd_eq_conj_irr1 // id_cht; apply/eqP.
-have F1: ('chi_t ^ (g ^+ 2))%CF = 'chi_t.
-  rewrite (cfConjgM _ nsHG) // -id_cht -conj_cfConjg -id_cht.
-  exact: cfConjCK.
-suffices /eqP->: g == ((g ^+ 2) ^+ #|G|./2.+1)%g.
-  elim: _./2.+1 => [|n IHn]; first exact: cfConjgJ1.
-  by rewrite expgS (cfConjgM _ nsHG) ?groupX // F1.
-rewrite eq_mulVg1 expgS -expgM mul2n -mulgA mulKg -expgS -order_dvdn.
-by rewrite -add1n -[1%N](congr1 nat_of_bool oddG) odd_double_half order_dvdG.
-Qed.
-
-(* This is Peterfalvi (1.6)(a). *)
-Lemma sub_cfker_Ind_irr A i :
-    H \subset G -> G \subset 'N(A) ->
-  (A \subset cfker ('Ind[G, H] 'chi_i)) = (A \subset cfker 'chi_i).
-Proof. by move=> sHG nAG; rewrite cfker_Ind_irr ?sub_gcore. Qed.
-
-(* Some consequences and related results. *)
-Lemma sub_cfker_Ind (A : {set gT}) chi :
-    A \subset H -> H \subset G -> G \subset 'N(A) -> chi \is a character ->
-  (A \subset cfker ('Ind[G, H] chi)) = (A \subset cfker chi).
-Proof.
-move=> sAH sHG nAG Nchi; have [-> | nz_chi] := eqVneq chi 0.
-  by rewrite raddf0 !cfker_cfun0 !(subset_trans sAH).
-by rewrite cfker_Ind ?sub_gcore.
-Qed.
-
-Lemma cfInd_irr_eq1 i :
-  H <| G -> ('Ind[G, H] 'chi_i == 'Ind[G, H] 1) = (i == 0).
-Proof.
-case/andP=> sHG nHG; apply/eqP/idP=> [chi1 | /eqP->]; last by rewrite irr0.
-rewrite -subGcfker -(sub_cfker_Ind_irr _ sHG nHG) chi1 -irr0.
-by rewrite sub_cfker_Ind_irr ?cfker_irr0.
-Qed.
-
-Lemma sub_cfker_constt_Res_irr (A : {set gT}) i j :
-    j \in irr_constt ('Res[H, G] 'chi_i) ->
-    A \subset H -> H \subset G -> G \subset 'N(A) ->
-  (A \subset cfker 'chi_j) = (A \subset cfker 'chi_i).
-Proof.
-move=> iHj sAH sHG nAG; apply/idP/idP=> kerA.
-  have jGi: i \in irr_constt ('Ind 'chi_j) by rewrite constt_Ind_Res.
-  rewrite (subset_trans _ (cfker_constt _ jGi)) ?cfInd_char ?irr_char //=.
-  by rewrite sub_cfker_Ind_irr.
-rewrite (subset_trans _ (cfker_constt _ iHj)) ?cfRes_char ?irr_char //=.
-by rewrite cfker_Res ?irr_char // subsetI sAH.
-Qed.
-
-Lemma sub_cfker_constt_Ind_irr (A : {set gT}) i j :
-    i \in irr_constt ('Ind[G, H] 'chi_j) ->
-    A \subset H -> H \subset G -> G \subset 'N(A) ->
-  (A \subset cfker 'chi_j) = (A \subset cfker 'chi_i).
-Proof. by rewrite constt_Ind_Res; apply: sub_cfker_constt_Res_irr. Qed.
-
-(* This is a stronger version of Peterfalvi (1.6)(b). *)
-Lemma cfIndMod (K : {group gT}) (phi : 'CF(H / K)) :
-    K \subset H -> H \subset G -> K <| G ->
-  'Ind[G] (phi %% K)%CF = ('Ind[G / K] phi %% K)%CF.
-Proof. by move=> sKH sHG /andP[_ nKG]; rewrite cfIndMorph ?ker_coset. Qed.
-
-Lemma cfIndQuo (K : {group gT}) (phi : 'CF(H)) :
-    K \subset cfker phi -> H \subset G -> K <| G ->
-  'Ind[G / K] (phi / K)%CF = ('Ind[G] phi / K)%CF.
-Proof.
-move=> kerK sHG nsKG; have sKH := subset_trans kerK (cfker_sub phi).
-have nsKH := normalS sKH sHG nsKG.
-by apply: canRL (cfModK nsKG) _; rewrite -cfIndMod // cfQuoK.
-Qed.
-
-Section IndSumInertia.
-
-Variable s : Iirr H.
-
-Let theta := 'chi_s.
-Let T := 'I_G[theta].
-Let calA := irr_constt ('Ind[T] theta).
-Let calB := irr_constt ('Ind[G] theta).
-Let AtoB (t : Iirr T) := Ind_Iirr G t.
-Let e_ t := '['Ind theta, 'chi[T]_t].
-
-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 *)
-
-(* This is Peterfalvi (1.7)(a). *)
-Lemma cfInd_sum_Inertia :
-  [/\ {in calA, forall t, 'Ind 'chi_t \in irr G},
-      {in calA, forall t, 'chi_(AtoB t) = 'Ind 'chi_t},
-      {in calA &, injective AtoB},
-      AtoB @: calA =i calB
-    & 'Ind[G] theta = \sum_(t in calA) e_ t *: 'Ind 'chi_t].
-Proof.
-have [AtoBirr AtoBinj defB _ _] := constt_Inertia_bijection s nsHG.
-split=> // [i Ai|]; first exact/cfIirrE/AtoBirr.
-rewrite -(cfIndInd _ sTG sHT) {1}['Ind theta]cfun_sum_constt linear_sum.
-by apply: eq_bigr => i _; rewrite linearZ.
-Qed.
-
-Hypothesis abTbar : abelian (T / H).
-
-(* 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}].
-Proof.
-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.
-have LtoTE j: 'chi_(LtoT j) = ('chi_j %% H)%CF * psi1.
-  by rewrite !(mod_IirrE, cfIirrE) // mul_lin_irr ?mem_irr ?cfMod_lin_char.
-have psiHG: 'Ind ('Res[H] psi1) = \sum_j 'chi_(LtoT j).
-  transitivity ((cfReg (T / H) %% H)%CF * psi1); last first.
-    rewrite cfReg_sum linear_sum /= mulr_suml; apply: eq_bigr => i _.
-    by rewrite LtoTE // lin_char1 ?scale1r.
-  apply/cfun_inP=> x Tx; rewrite cfunE cfModE // cfRegE mulrnAl mulrb.
-  rewrite (sameP eqP (kerP _ (subsetP nHT x Tx))) ker_coset.
-  case: ifPn => [Hx | H'x]; last by rewrite (cfun_on0 (cfInd_normal _  _)).
-  rewrite card_quotient // -!(cfResE _ sHT) // cfRes_Ind_invariant ?cfunE //.
-  by rewrite -subsetIidl (subset_trans _ (sub_inertia_Res _ _)) ?sub_Inertia.
-have imLtoT: {subset calA <= codom LtoT}.
-  move=> t At; apply/codomP/exists_eqP.
-  have{At}: t \in irr_constt ('Ind ('Res[H] 'chi_t1)).
-    by rewrite Dpsi1H linearZ irr_consttE cfdotZl mulf_neq0.
-  apply: contraR; rewrite negb_exists => /forallP imL't.
-  by rewrite psiHG cfdot_suml big1 // => j _; rewrite cfdot_irr mulrb ifN_eqC.
-have De_ t: t \in calA -> e_ t = e.
-  case/imLtoT/codomP=> j ->; rewrite /e_ LtoTE /e -!cfdot_Res_r rmorphM /=.
-  by rewrite cfRes_sub_ker ?cfker_mod // mulr_algl lin_char1 ?scale1r.
-have{imLtoT} A_1 t: t \in calA -> 'chi_t 1%g = e * theta 1%g.
-  case/imLtoT/codomP=> j ->; rewrite LtoTE //= cfunE.
-  by rewrite (lin_char1 (linLH j)) mul1r -(cfRes1 H) Dpsi1H cfunE.
-exists e => //; have [_ defAtoB injAtoB imAtoB ->] := cfInd_sum_Inertia.
-rewrite -(eq_bigl _ _ imAtoB) -(eq_card imAtoB) big_imset //= scaler_sumr.
-split=> [||i]; first by apply: eq_bigr => t2 At2; rewrite De_ ?defAtoB.
-  apply: (mulIf (irr1_neq0 s)); rewrite mulrAC -cfInd1 // mulr_natl mulrC invfM.
-  rewrite ['Ind _]cfun_sum_constt sum_cfunE mulr_sumr card_in_imset //.
-  rewrite -sumr_const; apply: eq_bigr => t At.
-  by rewrite -mulrA -/(e_ t) De_ // cfunE A_1 ?mulKf.
-by rewrite -imAtoB => /imsetP[t At ->]; rewrite defAtoB ?cfInd1 ?A_1 ?mulrA.
-Qed.
-
-(* This is Peterfalvi (1.7)(c). *)
-Lemma cfInd_Hall_central_Inertia :
-     Hall T H ->
-  [/\ 'Ind[G] theta = \sum_(i in calB) 'chi_i, #|calB| = #|T : H| 
-    & {in calB, forall i, 'chi_i 1%g = #|G : T|%:R * theta 1%g}].
-Proof.
-case/andP=> _ hallH; have [e [_ _ De]] := cfInd_central_Inertia.
-suffices ->: e = 1.
-  by case=> -> /eqP; rewrite scale1r expr1n divr1 mulr1 eqC_nat => /eqP.
-suffices{De} [t Dtheta]: exists i, 'Res[H, T] 'chi_i = theta.
-  have e_t_1: e_ t = 1 by rewrite /e_ -cfdot_Res_r Dtheta cfnorm_irr.
-  by rewrite -(De t) // irr_consttE -/(e_ t) e_t_1 oner_eq0.
-have ITtheta: T \subset 'I[theta] := subsetIr _ _.
-have solT: solvable (T / H) := abelian_sol abTbar.
-have [|t []] := extend_solvable_coprime_irr nsHT solT ITtheta; last by exists t.
-rewrite coprime_sym coprime_mull !(coprime_dvdl _ hallH) ?cfDet_order_dvdG //.
-by rewrite -dvdC_nat !CdivE truncCK ?Cnat_irr1 // dvd_irr1_cardG.
-Qed.
-  
-End IndSumInertia.
-
-(* This is Peterfalvi (1.8). *)
-Lemma irr1_bound_quo (B C D : {group gT}) i :
-    B <| C -> B \subset cfker 'chi[G]_i ->
-    B \subset D -> D \subset C -> C \subset G -> (D / B \subset 'Z(C / B))%g ->
-  'chi_i 1%g <= #|G : C|%:R * sqrtC #|C : D|%:R.
-Proof.
-move=> BnC BsK BsD DsC CsG QsZ.
-case: (boolP ('Res[C] 'chi_i == 0))=> [HH|].
-  have: ('Res[C] 'chi_i) 1%g = 0 by rewrite (eqP HH) cfunE.
-  by rewrite cfResE // => HH1; case/eqP: (irr1_neq0 i).
-have IC := cfRes_char C (irr_char i).
-case/neq0_has_constt=> i1 Hi1.
-have CIr: i \in irr_constt ('Ind[G] 'chi_i1).
-  by rewrite inE /= -Frobenius_reciprocity /= cfdotC conjC_eq0.
-have BsKi : B \subset cfker 'chi_i1.
-  suff BsKri: B \subset cfker ('Res[C] 'chi_i).
-    by apply: (subset_trans BsKri); apply: (cfker_constt _ Hi1).
-  apply/subsetP=> g GiG.
-  have F: g \in C by rewrite (subsetP (subset_trans BsD _)).
-  rewrite cfkerEchar // inE F !cfResE //.
-  by move: (subsetP BsK _ GiG); rewrite cfkerEirr inE.
-pose i2 := quo_Iirr B i1.
-have ZsC: 'Z(C / B)%g \subset 'Z('chi_i2)%CF.
-    by rewrite -(cap_cfcenter_irr (C / B)); apply: bigcap_inf.
-have CBsH: C :&: B \subset D.
-    apply/subsetP=> g; rewrite inE; case/andP=> _ HH.
-    by apply: (subsetP (BsD)).
-have I1B: 'chi_i1 1%g ^+ 2 <= #|C : D|%:R.
-  case: (irr1_bound i2)=> HH _; move: HH.
-  have ->: 'chi_i2 1%g = 'chi_i1 1%g.
-    by rewrite quo_IirrE // -(coset_id (group1 B)) cfQuoE.
-  move/ler_trans; apply.
-  rewrite ler_nat // -(index_quotient_eq CBsH) ?normal_norm //.
-  rewrite -(@leq_pmul2l #|'Z('chi_i2)%CF|) ?cardG_gt0 ?cfcenter_sub //.
-  rewrite Lagrange ?quotientS ?cfcenter_sub //.
-  rewrite -(@leq_pmul2l #|(D / B)%g|) ?cardG_gt0 //.
-  rewrite mulnA mulnAC Lagrange ?quotientS //.
-  rewrite mulnC leq_pmul2l ?cardG_gt0 // subset_leq_card //.
-  exact: subset_trans QsZ ZsC.
-have IC': 'Ind[G] 'chi_i1 \is a character := cfInd_char G (irr_char i1).
-move: (char1_ge_constt IC' CIr); rewrite cfInd1 //= => /ler_trans-> //.
-have chi1_1_ge0: 0 <= 'chi_i1 1%g by rewrite ltrW ?irr1_gt0.
-rewrite ler_pmul2l ?gt0CiG //.
-by rewrite -(@ler_pexpn2r _ 2) -?topredE /= ?sqrtC_ge0 ?ler0n ?sqrtCK.
-Qed.
-
-(* This is Peterfalvi (1.9)(a). *)
-Lemma extend_coprime_Qn_aut a b (Qa Qb : fieldExtType rat) w_a w_b
-          (QaC : {rmorphism Qa -> algC}) (QbC : {rmorphism Qb -> algC})
-          (mu : {rmorphism algC -> algC}) :
-    coprime a b ->
-    a.-primitive_root w_a /\ <<1; w_a>>%VS = {:Qa}%VS -> 
-    b.-primitive_root w_b /\ <<1; w_b>>%VS = {:Qb}%VS ->
-  {nu : {rmorphism algC -> algC} | forall x, nu (QaC x) = mu (QaC x)
-                                 & forall y, nu (QbC y) = QbC y}.
-Proof.
-move=> coab [pr_w_a genQa] [pr_w_b genQb].
-have [k co_k_a Dmu]: {k | coprime k a & mu (QaC w_a) = QaC (w_a ^+ k)}.
-  have prCw: a.-primitive_root (QaC w_a) by rewrite fmorph_primitive_root.
-  by have [k coka ->] := aut_prim_rootP mu prCw; rewrite -rmorphX; exists k.
-pose k1 := chinese a b k 1; have /Qn_aut_exists[nu Dnu]: coprime k1 (a * b).
-  rewrite coprime_mulr -!(coprime_modl k1) chinese_modl ?chinese_modr //.
-  by rewrite !coprime_modl co_k_a coprime1n.
-exists nu => [x | y].
-  have /Fadjoin_polyP[p Qp ->]: x \in <<1; w_a>>%VS by rewrite genQa memvf.
-  rewrite -!horner_map -!map_poly_comp !map_Qnum_poly // Dmu Dnu -rmorphX /=.
-    by rewrite -(prim_expr_mod pr_w_a) chinese_modl // prim_expr_mod.
-  by rewrite exprM (prim_expr_order pr_w_a) expr1n rmorph1.
-have /Fadjoin_polyP[p Qp ->]: y \in <<1; w_b>>%VS by rewrite genQb memvf.
-rewrite -!horner_map -!map_poly_comp !map_Qnum_poly // Dnu -rmorphX /=.
-  by rewrite -(prim_expr_mod pr_w_b) chinese_modr // prim_expr_mod.
-by rewrite mulnC exprM (prim_expr_order pr_w_b) expr1n rmorph1.
-Qed.
-
-(* This intermediate result in the proof of Peterfalvi (1.9)(b) is used in    *)
-(* he proof of (3.9)(c).                                                      *)
-Lemma dvd_restrict_cfAut a (v : {rmorphism algC -> algC}) :
-  exists2 u : {rmorphism algC -> algC},
-    forall gT0 G0 chi x,
-      chi \in 'Z[irr (@gval gT0 G0)] -> #[x] %| a -> u (chi x) = v (chi x)
-  & forall chi x, chi \in 'Z[irr G] -> coprime #[x] a -> u (chi x) = chi x.
-Proof.
-have [-> | a_gt0] := posnP a.
-  exists v => // chi x Zchi; rewrite /coprime gcdn0 order_eq1 => /eqP->.
-  by rewrite aut_Cint ?Cint_vchar1.
-pose b := (#|G|`_(\pi(a)^'))%N.
-have co_a_b: coprime a b := pnat_coprime (pnat_pi a_gt0) (part_pnat _ _).
-have [Qa _ [QaC _ [w_a genQa memQa]]] := group_num_field_exists [group of Zp a].
-have [Qb _ [QbC _ [w_b genQb memQb]]] := group_num_field_exists [group of Zp b].
-rewrite !card_Zp ?part_gt0 // in Qa QaC w_a genQa memQa Qb QbC w_b genQb memQb.
-have [nu nuQa nuQb] := extend_coprime_Qn_aut QaC QbC v co_a_b genQa genQb.
-exists nu => [gt0 G0 chi x Zchi x_dv_a | chi x Zchi co_x_a].
-  without loss{Zchi} Nchi: chi / chi \is a character.
-    move=> IH; case/vcharP: Zchi => [chi1 Nchi1 [chi2 Nchi2 ->]].
-    by rewrite !cfunE !rmorphB !IH.
-  by have [xa <-] := memQa _ _ _ Nchi x x_dv_a; rewrite nuQa.
-without loss{Zchi} Nchi: chi / chi \is a character.
-  move=> IH; case/vcharP: Zchi => [chi1 Nchi1 [chi2 Nchi2 ->]].
-  by rewrite !cfunE rmorphB !IH.
-have [Gx | /cfun0->] := boolP (x \in G); last by rewrite rmorph0.
-have{Gx} x_dv_b: (#[x] %| b)%N.
-  rewrite coprime_sym coprime_pi' // in co_x_a.
-  by rewrite -(part_pnat_id co_x_a) partn_dvd ?order_dvdG.
-by have [xb <-] := memQb _ _ _ Nchi x x_dv_b; rewrite nuQb.
-Qed.
-
-(* This is Peterfalvi (1.9)(b). *)
-(* We have strengthened the statement of this lemma so that it can be used    *)
-(* rather than reproved for Peterfalvi (3.9). In particular we corrected a    *)
-(* quantifier inversion in the original statement: the automorphism is        *)
-(* constructed uniformly for all (virtual) characters. We have also removed   *)
-(* the spurrious condition that a be a \pi(a) part of #|G| -- the proof works *)
-(* for all a, and indeed the first part holds uniformaly for all groups!      *)
-Lemma make_pi_cfAut a k :
-    coprime k a ->
-  exists2 u : {rmorphism algC -> algC},
-    forall (gT0 : finGroupType) (G0 : {group gT0}) chi x,
-      chi \in 'Z[irr G0] -> #[x] %| a -> cfAut u chi x = chi (x ^+ k)%g
-  & forall chi x, chi \in 'Z[irr G] -> coprime #[x] a -> cfAut u chi x = chi x.
-Proof.
-move=> co_k_a; have [v Dv] := Qn_aut_exists co_k_a.
-have [u Du_a Du_a'] := dvd_restrict_cfAut a v.
-exists u => [gt0 G0 | ] chi x Zchi a_x; last by rewrite cfunE Du_a'.
-rewrite cfunE {u Du_a'}Du_a //.
-without loss{Zchi} Nchi: chi / chi \is a character.
-  move=> IH; case/vcharP: Zchi => [chi1 Nchi1 [chi2 Nchi2 ->]].
-  by rewrite !cfunE rmorphB !IH.
-have [sXG0 | G0'x] := boolP (<[x]> \subset G0); last first.
-  have /(<[x]> =P _) gen_xk: generator <[x]> (x ^+ k).
-    by rewrite generator_coprime coprime_sym (coprime_dvdr a_x).
-  by rewrite !cfun0 ?rmorph0 -?cycle_subG -?gen_xk.
-rewrite -!(cfResE chi sXG0) ?cycle_id ?mem_cycle //.
-rewrite ['Res _]cfun_sum_cfdot !sum_cfunE rmorph_sum; apply: eq_bigr => i _.
-have chiX := lin_charX (char_abelianP _ (cycle_abelian x) i) _ (cycle_id x).
-rewrite !cfunE rmorphM aut_Cnat ?Cnat_cfdot_char_irr ?cfRes_char //.
-by congr (_ * _); rewrite Dv -chiX // -expg_mod_order (eqnP a_x) chiX.
-Qed.
-
-Section ANT.
-Import ssrint.
-
-(* This section covers Peterfalvi (1.10). *)
-(* We have simplified the statement somewhat by substituting the global ring  *)
-(* of algebraic integers for the specific ring Z[eta]. Formally this amounts  *)
-(* to strengthening (b) and weakening (a) accordingly, but since actually the *)
-(* Z[eta] is equal to the ring of integers of Q[eta] (cf. Theorem 6.4 in J.S. *)
-(* Milne's course notes on Algebraic Number Theory), the simplified statement *)
-(* is actually equivalent to the textbook one.                                *)
-Variable (p : nat) (eps : algC).
-Hypothesis (pr_eps : p.-primitive_root eps).
-Local Notation e := (1 - eps).
-
-(* This is Peterfalvi (1.10) (a). *)
-Lemma vchar_ker_mod_prim : {in G & G & 'Z[irr G], forall x y (chi : 'CF(G)),
-  #[x] = p -> y \in 'C[x] -> chi (x * y)%g == chi y %[mod e]}%A.
-Proof.
-move=> x y chi Gx Gy Zchi ox cxy; pose X := <<[set x; y]>>%G.
-have [Xx Xy]: x \in X /\ y \in X by apply/andP; rewrite -!sub1set -join_subG.
-have sXG: X \subset G by rewrite join_subG !sub1set Gx.
-suffices{chi Zchi} IHiX i: ('chi[X]_i (x * y)%g == 'chi_i y %[mod e])%A.
-  rewrite -!(cfResE _ sXG) ?groupM //.
-  have irr_free := (free_uniq (basis_free (irr_basis X))).
-  have [c Zc ->] := (zchar_expansion irr_free (cfRes_vchar X Zchi)).
-  rewrite !sum_cfunE /eqAmod -sumrB big_seq rpred_sum // => _  /irrP[i ->].
-  by rewrite !cfunE [(_ %| _)%A]eqAmodMl // rpred_Cint.
-have lin_chi: 'chi_i \is a linear_char.
-  apply/char_abelianP; rewrite -[gval X]joing_idl -joing_idr abelianY.
-  by rewrite !cycle_abelian cycle_subG /= cent_cycle.
-rewrite lin_charM // -{2}['chi_i y]mul1r eqAmodMr ?Aint_irr //.
-have [|k ->] := (prim_rootP pr_eps) ('chi_i x).
-  by rewrite -lin_charX // -ox expg_order lin_char1.
-rewrite -[_ ^+ k](subrK 1) subrX1 -[_ - 1]opprB mulNr -mulrN mulrC.
-rewrite eqAmod_addl_mul // rpredN rpred_sum // => n _.
-by rewrite rpredX ?(Aint_prim_root pr_eps).
-Qed.
-
-(* This is Peterfalvi (1.10)(b); the primality condition is only needed here. *)
-Lemma int_eqAmod_prime_prim n :
-  prime p -> n \in Cint -> (n == 0 %[mod e])%A -> (p %| n)%C.
-Proof.
-move=> p_pr Zn; rewrite /eqAmod unfold_in subr0.
-have p_gt0 := prime_gt0 p_pr.
-case: ifPn => [_ /eqP->// | nz_e e_dv_n].
-suffices: (n ^+ p.-1 == 0 %[mod p])%A.
-  rewrite eqAmod0_rat ?rpredX ?rpred_nat 1?rpred_Cint // !dvdC_int ?rpredX //.
-  by rewrite floorCX // abszX Euclid_dvdX // => /andP[].
-rewrite /eqAmod subr0 unfold_in pnatr_eq0 eqn0Ngt p_gt0 /=.
-pose F := \prod_(1 <= i < p) ('X - (eps ^+ i)%:P).
-have defF: F = \sum_(i < p) 'X^i.
-  apply: (mulfI (monic_neq0 (monicXsubC 1))); rewrite -subrX1.
-  by rewrite -(factor_Xn_sub_1 pr_eps) big_ltn.
-have{defF} <-: F.[1] = p :> Algebraics.divisor.
-  rewrite -[p]card_ord -[rhs in _ = rhs]sumr_const defF horner_sum.
-  by apply: eq_bigr => i _; rewrite hornerXn expr1n.
-rewrite -[p.-1]card_ord {F}horner_prod big_add1 big_mkord -prodfV.
-rewrite -prodr_const -big_split rpred_prod //= => k _; rewrite !hornerE.
-rewrite -[n](divfK nz_e) -[_ * _ / _]mulrA rpredM {e_dv_n}//.
-have p'k: ~~ (p %| k.+1)%N by rewrite gtnNdvd // -{2}(prednK p_gt0) ltnS.
-have [r {1}->]: exists r, eps = eps ^+ k.+1 ^+ r.
-  have [q _ /dvdnP[r Dr]] := Bezoutl p (ltn0Sn k); exists r; apply/esym/eqP.
-  rewrite -exprM (eq_prim_root_expr pr_eps _ 1) mulnC -Dr addnC gcdnC.
-  by rewrite -prime_coprime // in p'k; rewrite (eqnP p'k) modnMDl.
-rewrite -[1 - _]opprB subrX1 -mulNr opprB mulrC.
-rewrite mulKf; last by rewrite subr_eq0 eq_sym -(prim_order_dvd pr_eps).
-by apply: rpred_sum => // i _; rewrite !rpredX ?(Aint_prim_root pr_eps).
-Qed.
-
-End ANT.
-
-End Main.
-
-