simp [hp]
case neg.h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
m : ι →₀ ℕ
hm : ¬m = 0
h : ¬coeff m p = 0
hp : ∀ (x : ι), m x = 0
a✝ : ι
⊢ m a✝ = 0 a✝
no goals