proposition: 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: 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 coprimeMl !(coprime_dvdl _ hallH) ?cfDet_order_dvdG //. by rewrite -dvdC_nat !CdivE truncCK ?Cnat_irr1 // dvd_irr1_cardG. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice fintype) mathcomp(tuple finfun bigop prime order ssralg finset fingroup morphism) mathcomp(perm automorphism quotient action zmodp finalg center commutator) mathcomp(poly cyclic pgroup nilpotent matrix mxalgebra mxrepresentation) mathcomp(vector falgebra fieldext ssrnum algC rat algnum galois) mathcomp(classfun character inertia integral_char vcharacter)