case a
X : Type u_1
k : ℤ
h : k ≠ 0
a : FreeAbelianGroup X
x : X
⊢ x ∈ support (k • a) ↔ x ∈ support a
X : Type u_1
k : ℤ
h : k ≠ 0
a : FreeAbelianGroup X
⊢ support (k • a) = support a
ext x
case a
X : Type u_1
k : ℤ
h : k ≠ 0
a : FreeAbelianGroup X
x : X
⊢ k • ↑(coeff x) a ≠ 0 ↔ ↑(coeff x) a ≠ 0
case a
X : Type u_1
k : ℤ
h : k ≠ 0
a : FreeAbelianGroup X
x : X
⊢ x ∈ support (k • a) ↔ x ∈ support a
simp only [mem_support_iff, AddMonoidHom.map_zsmul]
no goals
case a
X : Type u_1
k : ℤ
h : k ≠ 0
a : FreeAbelianGroup X
x : X
⊢ k • ↑(coeff x) a ≠ 0 ↔ ↑(coeff x) a ≠ 0
simp only [h, zsmul_int_int, false_or_iff, Ne.def, mul_eq_zero]