letI := Classical.decEq ι
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree = 0
⊢ p = C (coeff 0 p)
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)