proposition: Lemma pihomog_mPo p d : pihomog mdeg d (p \mPo S) = pihomog mnmwgt d p \mPo S.
proof: Proof. elim/mpolyind: p; first by rewrite !linear0. move=> c m p msupp cn0 ihp; rewrite !linearP /= {}ihp. congr (c *: _ + _); case: (eqVneq (mnmwgt m) d) => wgtm. + have /eqP := wgtm; rewrite -(dhomogX R) => /pihomog_dE ->. by have := dhomog_XS m; rewrite wgtm => /pihomog_dE ->. rewrite (pihomog_ne0 wgtm (dhomog_XS m)). by rewrite (pihomog_ne0 wgtm) ?linear0 // dhomogX. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(order fingroup perm ssralg zmodp poly ssrint) mathcomp(matrix vector) mathcomp(bigenough) ssrcomplements freeg