proposition: Theorem LR_rule_irrSG c d (la : 'P_c) (mu : 'P_d) : 'Ind['SG_(c + d)] ('irrSG[la] \o^ 'irrSG[mu]) = \sum_(nu : 'P_(c + d) | included la nu) 'irrSG[nu] *+ LRyam_coeff la mu nu.
proof: Proof. apply (can_inj (FcharK (leqSpred (c + d)))). rewrite Fchar_ind_morph linear_sum //= !Fchar_irrSGE. apply val_inj; rewrite /= linear_sum /=. rewrite syms_symsM; apply eq_bigr => nu _. by rewrite !linearMn /= Fchar_invK // leqSpred. 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