letI := Classical.decEq ι
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
⊢ (homogenization i p).IsHomogeneous p.totalDegree
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
⊢ (homogenization i p).IsHomogeneous p.totalDegree