proposition: Theorem Fchar_ind_morph m n (f : 'CF('SG_m)) (g : 'CF('SG_n)) : Fchar ('Ind['SG_(m + n)] (f \o^ g)) = Fchar f *h Fchar g.
proof: Proof. Proof using. rewrite (ncfuniCT_gen f) (ncfuniCT_gen g) !linear_sum; apply eq_bigr => /= l _. rewrite cfextprod_suml homsymprod_suml !linear_sum; apply eq_bigr => /= k _. do 2 rewrite [in RHS]linearZ /= Fchar_ncfuniCT. rewrite cfextprodZr cfextprodZl homsymprodZr homsymprodZl !scalerA. rewrite 2!linearZ /= ncfuniCT_Ind linearZ /= Fchar_ncfuniCT /=; congr (_ *: _). by apply val_inj => /=; rewrite prod_genM. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism gproduct) mathcomp(rat ssralg ssrint ssrnum algC vector archimedean) mathcomp(mxrepresentation classfun character) mathcomp(mpoly) sorted ordtype tools partition antisym sympoly homogsym Cauchy Schur_altdef stdtab therule permcomp cycletype towerSn permcent reprSn unitriginv MurnaghanNakayama