classical
apply homogenization_of_isHomogeneous p.totalDegree
exact isHomogeneous_homogenization _ _
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
⊢ homogenization i (homogenization i p) = homogenization i p
no goals