proposition: Lemma evalXY_homog d p : p \is d.-homog -> p(XY) \is d.-homog.
proof: Proof. move/pihomog_dE <-; rewrite pihomogE. rewrite rmorph_sum /=; apply rpred_sum => mon /eqP Hdeg. rewrite linearZ /= scale_polXYE; apply rpredZ. rewrite evalXY_XE -rmorph_prod /= polyXY_scale; apply rpredZ. by rewrite /polX_XY map_mpolyX dhomogX /= mdeg_monX Hdeg. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssrint rat ssralg ssrnum algC matrix vector) mathcomp(mpoly) tools partition ordtype antisym Schur_mpoly Schur_altdef sympoly homogsym permcent