proposition: Lemma Young_rule_partdom la : 'M[la] = 'irrSG[la] + \sum_(mu | (la < mu :> 'PDom_n)%O) 'K(mu, la) *: 'irrSG[mu].
proof: Proof. rewrite Young_rule. exact: (unitrig_sum1lV (fun mu : 'PDom_n => 'irrSG[mu]) la (Kostka_unitrig _ n)). 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