X : Type u_1
k : ℕ
h : k ≠ 0
a : FreeAbelianGroup X
⊢ ↑k ≠ 0
X : Type u_1
k : ℕ
h : k ≠ 0
a : FreeAbelianGroup X
⊢ support (k • a) = support a
apply support_zsmul k _ a
no goals
X : Type u_1
k : ℕ
h : k ≠ 0
a : FreeAbelianGroup X
⊢ ↑k ≠ 0
exact_mod_cast h