no goals
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
x : α
⊢ x ∈ toAList f ↔ ↑f x ≠ 0
classical rw [AList.mem_keys, ← List.mem_toFinset, toAList_keys_toFinset, mem_support_iff]
no goals
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
x : α
⊢ x ∈ toAList f ↔ ↑f x ≠ 0
rw [AList.mem_keys, ← List.mem_toFinset, toAList_keys_toFinset, mem_support_iff]