proposition: Lemma Schur_rowpartn d : \sum_(m : 'X_{1..n < d.+1} | mdeg m == d) 'X_[m] = Schur n0 R (rowpartn d).
proof: Proof. Proof using. rewrite -symh_basisE. transitivity (\sum_(m <- [seq s2m (tval s) | s in basis n d]) 'X_[m] : {mpoly R[n]}); last by rewrite big_map big_enum. rewrite (perm_big _ (perm_enum_basis d)) big_map big_enum /=. by apply eq_bigl => m; rewrite inE. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg) mathcomp(ssrcomplements freeg mpoly) tools ordtype partition tableau