proposition: 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: 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.
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)