rw [support_sum_monomial_coeff p]
case mpr
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h : p.IsHomogeneous p.totalDegree
⊢ ∑ d ∈ p.support, (monomial d) (coeff d p) = p
no goals