no goals
α : Type u_1
β : Type ?u.20446
γ : Type ?u.20449
ι : Type ?u.20452
M : Type u_2
M' : Type ?u.20458
N : Type ?u.20461
P : Type ?u.20464
G : Type ?u.20467
H : Type ?u.20470
R : Type ?u.20473
S : Type ?u.20476
inst✝ : Zero M
f : α →₀ M
⊢ card f.support = 0 ↔ f = 0
simp