proposition: Lemma sym_fundamental_symh (p : {mpoly R[n]}) : p \is symmetric -> { t | t \mPo S = p }.
proof: Proof. move=> psym. set f := omegasf (SymPoly psym). have [g [geq gwght]] := sym_fundamental (sympolP f). exists g; apply esym; apply/eqP. by rewrite (omegasf_compsymh (SymPoly psym) g) geq. 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