rw [support_sum_monomial_eq]
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
S : Finset (ι →₀ ℕ)
f : (ι →₀ ℕ) → R
⊢ (∑ v ∈ S, (monomial v) (f v)).support ⊆ S
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
S : Finset (ι →₀ ℕ)
f : (ι →₀ ℕ) → R
⊢ filter (fun v => f v ≠ 0) S ⊆ S