no goals
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_2
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
p✝ q : MvPolynomial σ R
A : Type u_1
inst✝ : AddCommMonoid A
p : MvPolynomial σ R
b : (σ →₀ ℕ) → R → A
⊢ sum p b = ∑ m in support p, b m (coeff m p)
simp [support, Finsupp.sum, coeff]