erw [Finset.sup_eq_bot_iff] at hp
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree = 0
this : DecidableEq ι := Classical.decEq ι
⊢ p = C (coeff 0 p)
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : ∀ s ∈ p.support, (s.sum fun x e => e) = ⊥
this : DecidableEq ι := Classical.decEq ι
⊢ p = C (coeff 0 p)