proposition: Lemma Clifford_Res_sum_cfclass i j : H <| G -> j \in irr_constt ('Res[H, G] 'chi_i) -> 'Res[H] 'chi_i = '['Res[H] 'chi_i, 'chi_j] *: (\sum_(chi <- ('chi_j ^: G)%CF) chi).
proof: Proof. move=> nsHG chiHj; have [sHG /subsetP nHG] := andP nsHG. rewrite reindex_cfclass //= big_mkcond. rewrite {1}['Res _]cfun_sum_cfdot linear_sum /=; apply: eq_bigr => k _. have [[y Gy ->] | ] := altP (cfclassP _ _ _); first by rewrite cfdot_Res_conjg. apply: contraNeq; rewrite scaler0 scaler_eq0 orbC => /norP[_ chiHk]. have{chiHk chiHj}: '['Res[H] ('Ind[G] 'chi_j), 'chi_k] != 0. rewrite !inE !cfdot_Res_l in chiHj chiHk *. apply: contraNneq chiHk; rewrite cfdot_sum_irr => /psumr_eq0P/(_ i isT)/eqP. rewrite -cfdotC cfdotC mulf_eq0 conjC_eq0 (negbTE chiHj) /= => -> // i1. by rewrite -cfdotC natr_ge0 // rpredM ?Cnat_cfdot_char ?cfInd_char ?irr_char. rewrite cfResInd // cfdotZl mulf_eq0 cfdot_suml => /norP[_]. apply: contraR => chiGk'j; rewrite big1 // => x Gx; apply: contraNeq chiGk'j. rewrite -conjg_IirrE cfdot_irr pnatr_eq0; case: (_ =P k) => // <- _. by rewrite conjg_IirrE; apply/cfclassP; exists x. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype div tuple finfun bigop prime order) mathcomp(ssralg ssrnum finset fingroup morphism perm) mathcomp(automorphism quotient action zmodp cyclic center) mathcomp(gproduct commutator gseries nilpotent pgroup) mathcomp(sylow maximal frobenius matrix mxalgebra) mathcomp(mxrepresentation vector algC classfun character) mathcomp(archimedean)