simp [hm]
case pos
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 = coeff m (C (coeff 0 p))
no goals