proposition: Corollary constt0_Res_cfker i : H <| G -> 0 \in irr_constt ('Res[H] 'chi[G]_i) -> H \subset cfker 'chi[G]_i.
proof: Proof. move=> nsHG /(Clifford_Res_sum_cfclass nsHG); have [sHG nHG] := andP nsHG. rewrite irr0 cfdot_Res_l cfclass1 // big_seq1 cfInd_cfun1 //. rewrite cfdotZr conjC_nat => def_chiH. apply/subsetP=> x Hx; rewrite cfkerEirr inE -!(cfResE _ sHG) //. by rewrite def_chiH !cfunE cfun11 cfun1E Hx. 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)