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