proposition: Lemma sym_fundamental_symh_homog (p : {mpoly R[n]}) (d : nat) : p \is symmetric -> p \is d.-homog -> { t | t \mPo S = p /\ t \is d.-homog for mnmwgt }.
proof: Proof. move=> psym Hhom. set f := omegasf (SymPoly psym). have sympol_homog : sympol f \is d.-homog by rewrite omegasf_homogE. have [g [geq ghom]] := sym_fundamental_homog (sympolP f) sympol_homog. exists g; split; last by []. 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