by_cases hpn : p = 0
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
i : ι
p : MvPolynomial ι R
hp : p.IsHomogeneous n
⊢ homogenization i p = p
case pos
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
i : ι
p : MvPolynomial ι R
hp : p.IsHomogeneous n
hpn : p = 0
⊢ homogenization i p = p

case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
i : ι
p : MvPolynomial ι R
hp : p.IsHomogeneous n
hpn : ¬p = 0
⊢ homogenization i p = p