proposition: Lemma omegasf_homog d : {homo omegasf: p / sympol p \in [in R[n], d.-homog]}.
proof: Proof. move=> p H; rewrite /omegasf /= homog_piE. have Hhom nv i : symh_pol nv R i \is i.-homog by apply symh_homog. have {Hhom} -> := pihomog_mPo Hhom. rewrite /sympolyf; case: (SF p) => [f [eqf _]]. by move: H; rewrite -{}eqf -mwmwgt_homogE homog_piE => /eqP ->. 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