case a
ι : Type u_1
R : Type ?u.2193
M : Type u_2
inst✝² : DecidableEq ι
inst✝¹ : Zero M
inst✝ : (m : M) → Decidable (m ≠ 0)
f : ι →₀ M
a✝ : ι
⊢ a✝ ∈ Dfinsupp.support (Finsupp.toDfinsupp f) ↔ a✝ ∈ f.support
ι : Type u_1
R : Type ?u.2193
M : Type u_2
inst✝² : DecidableEq ι
inst✝¹ : Zero M
inst✝ : (m : M) → Decidable (m ≠ 0)
f : ι →₀ M
⊢ Dfinsupp.support (Finsupp.toDfinsupp f) = f.support
ext
no goals
case a
ι : Type u_1
R : Type ?u.2193
M : Type u_2
inst✝² : DecidableEq ι
inst✝¹ : Zero M
inst✝ : (m : M) → Decidable (m ≠ 0)
f : ι →₀ M
a✝ : ι
⊢ a✝ ∈ Dfinsupp.support (Finsupp.toDfinsupp f) ↔ a✝ ∈ f.support
simp