proposition: Lemma cfdot_Ind_ncfuniCT p q (l : 'P_(m + n)) : '[ 'Ind['SG_(m + n)] ('1z_[p] \o^ '1z_[q]), '1z_[l] ] = (p +|+ q == l)%:R * 'z_l.
proof: Proof. Proof using. rewrite cfextprodZl cfextprodZr. rewrite !linearZ /= !cfdotZl cfdotZr cfdot_Ind_cfuniCT. case: eqP => _ /=; rewrite ?mul0r ?mulr0 // !mul1r. rewrite 2!mulrA mulrC mulrA [X in (X * _)]mulrC -invfM divff ?mul1r. by rewrite fmorph_div !conjC_nat. by apply mulf_neq0. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg fingroup morphism perm gproduct) mathcomp(ssrnum matrix vector mxalgebra algC) mathcomp(classfun character mxrepresentation) tools ordcast partition sorted permcomp cycles cycletype permcent