by_cases hp : p = 0
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
h : ∀ j ∈ p.support, j i = 0
⊢ (homogenization i p).totalDegree = p.totalDegree
case pos
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
h : ∀ j ∈ p.support, j i = 0
hp : p = 0
⊢ (homogenization i p).totalDegree = p.totalDegree

case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
h : ∀ j ∈ p.support, j i = 0
hp : ¬p = 0
⊢ (homogenization i p).totalDegree = p.totalDegree