proposition: Lemma mwmwgt_homogP (p : {mpoly R[n]}) d : reflect (forall nv, p \mPo E nv \is d.-homog) (p \is d.-homog for mnmwgt).
proof: Proof. Proof using. rewrite !homog_piE. apply (iffP eqP) => [Homog nv | H]. - by rewrite -Homog -(pihomog_mPo (fun nv i => dhomog_mesym nv R i)) pihomogP. - apply pihomog_dE. suff -> : p = pihomog mnmwgt d p by apply: pihomogP. apply msym_fundamental_un; apply esym. rewrite -(pihomog_mPo (fun nv i => dhomog_mesym nv R i)). exact: pihomog_dE. 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