proposition: Lemma pihomog_mPo nv p d : pihomog mdeg d (p \mPo G nv) = (pihomog mnmwgt d p) \mPo G nv.
proof: Proof. Proof using gen gen_homog. elim/mpolyind: p => [| c m p Hm Hc IHp] /=; first by rewrite !linear0. rewrite !linearP /= {}IHp; congr (c *: _ + _). case/altP: (mnmwgt m =P d) => Hd. - have/eqP := Hd; rewrite -(dhomogX R) => /pihomog_dE ->. by have:= homog_X_mPo_gen nv m; rewrite Hd => /pihomog_dE ->. - rewrite (pihomog_ne0 Hd (homog_X_mPo_gen nv m)). rewrite (pihomog_ne0 Hd); first by rewrite linear0. by rewrite dhomogX. 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