simp
case empty
R : Type u_1
ι : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq R
f : (ι →₀ ℕ) → R
this : DecidableEq ι := Classical.decEq ι
⊢ (∑ v ∈ ∅, (monomial v) (f v)).support = filter (fun v => f v ≠ 0) ∅
no goals