classical
by_contra h
specialize hp m h
apply hm
rw [Finsupp.sum] at hp
simp only [_root_.not_imp_self, bot_eq_zero, Finsupp.mem_support_iff, Finset.sum_eq_zero_iff] at hp
ext
simp [hp]
case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
hp : ∀ (s : ι →₀ ℕ), coeff s p ≠ 0 → (s.sum fun x e => e) = ⊥
m : ι →₀ ℕ
hm : ¬m = 0
⊢ coeff m p = 0
no goals