proposition: Theorem ncfuniCT_Ind p q : 'Ind['SG_(m + n)] ('1z_[p] \o^ '1z_[q]) = '1z_[p +|+ q].
proof: Proof. Proof using. apply/cfunP => /= x; rewrite cfunE. rewrite cfdotr_ncfuniCT cfdot_Ind_ncfuniCT. rewrite cfuniCTnE eq_sym mulrC. by case: (boolP (_ == _)) => [/eqP ->|] //=; rewrite !mulr0. 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