intro h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
⊢ homogenization i p ≠ 0
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hp : p ≠ 0
hjp : ∀ j ∈ p.support, j i = 0
h : homogenization i p = 0
⊢ False