Integer_Multiples_under_Addition_form_Infinite_Cyclic_Group
Provedcyclic-groupsgroup-theoryintegersmultiplesproofwiki
Let be the set of integer multiples of . Then is a countably infinite cyclic group. It is generated by and Hence can be justifiably referred to as the additive group of integer multiples.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Integer_Multiples_under_Addition_form_Infinite_Cyclic_Group (n : ℤ) (hn : n ≠ 0) : IsAddCyclic (AddSubgroup.closure ({n} : Set ℤ)) := by sorrySource