X : Type u_1
x : X
a : FreeAbelianGroup X
⊢ ↑(↑toFinsupp a) x = 0 ↔ ↑(coeff x) a = 0
X : Type u_1
x : X
a : FreeAbelianGroup X
⊢ ¬x ∈ support a ↔ ↑(coeff x) a = 0
rw [support, Finsupp.not_mem_support_iff]
no goals
X : Type u_1
x : X
a : FreeAbelianGroup X
⊢ ↑(↑toFinsupp a) x = 0 ↔ ↑(coeff x) a = 0
exact Iff.rfl