proposition: Lemma symh_basisE d : \sum_(s in basis n d) 'X_[s2m s] = Schur (rowpartn d).
proof: Proof. Proof using. rewrite Schur_tabsh_readingE (eq_bigl _ _ (@tabwordshape_row d)). under [LHS]eq_bigr do rewrite mons2mE. by apply eq_bigl => m; rewrite inE. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg) mathcomp(ssrcomplements freeg mpoly) tools ordtype partition tableau