proposition: Lemma sym_fundamental_homog (p : {mpoly R[n]}) (d : nat) : p \is symmetric -> p \is d.-homog -> { t | t \mPo (E n) = p /\ t \is d.-homog for mnmwgt }.
proof: Proof. move=> /sym_fundamental [t [Ht _]] Hhom. exists (pihomog mnmwgt d t); split. - by rewrite -(pihomog_mPo (fun nv i => dhomog_mesym nv R i)) Ht pihomog_dE. - exact: pihomogP. 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