proposition: Lemma expUmpartE nv k : (U_(ord0) *+ k)%MM = mpart (rowpartn k) :> 'X_{1..nv.+1}.
proof: Proof. rewrite rowpartnE. apply/mnmP => [[i Hi]]; rewrite /mpart mulmnE !mnmE -val_eqE /=. case: k => [|k] /=; first by rewrite muln0 mnmE nth_default. rewrite mnmE /=; by case: i {Hi} => [|i] //=; rewrite mul1n. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm) mathcomp(ssrcomplements freeg mpoly) sorted tools ordtype permuted partition skewpart composition Yamanouchi std tableau stdtab skewtab permcent antisym Schur_mpoly therule Schur_altdef unitriginv