proposition: Lemma Young_rule la : 'M[la] = \sum_(mu : 'P_n) 'K(mu, la) *: 'irrSG[mu].
proof: Proof. pose HS := {homsym algC[n.-1.+1, n]}. rewrite /YoungSG /irrSG. apply: (can_inj (FcharK _)); rewrite // Fchar_invK //. have -> : 'hh[la] = \sum_(mu : 'P_n) 'K(mu, la) *: 'hs[mu] :> HS. apply/val_inj; rewrite -[val 'hh[la]]/('h[la]). by rewrite /= symh_syms /= linear_sum /=. rewrite linear_sum /=; apply eq_bigr => mu hmu. by rewrite linearZ /= Fchar_invK. 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