proposition: Lemma omegasf_homogE d : {mono omegasf: p / sympol p \in [in R[n], d.-homog]}.
proof: Proof. move=> p; apply/idP/idP; last exact: omegasf_homog. by rewrite -{2}(omegasfK p); apply: omegasf_homog. 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