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.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