English
Structure theorem: any finitely generated abelian group is a finite direct sum of cyclic p-power groups ZMod(p^e).
Русский
Теорема о структуре: любую конечно-генерируемую абелеву группу можно разложить в конечную прямую сумму циклических групп ZMod(p^e).
LaTeX
$$$\exists ι\; (Fintype\; ι)\; (p: ι\to\mathbb{N})\; (e: ι\to\mathbb{N})\; G \cong_+ \bigl( \mathbb{Z}^n \oplus \bigoplus_{i\in ι} \mathbb{Z}/p_i^{e_i}\mathbb{Z} \bigr)$$$
Lean4
theorem finite_of_fg_torsion [AddCommGroup M] [Module ℤ M] [Module.Finite ℤ M] (hM : Module.IsTorsion ℤ M) :
_root_.Finite M := by
rcases Module.equiv_directSum_of_isTorsion hM with ⟨ι, _, p, h, e, ⟨l⟩⟩
haveI : ∀ i : ι, NeZero (p i ^ e i).natAbs := fun i => ⟨Int.natAbs_ne_zero.mpr <| pow_ne_zero (e i) (h i).ne_zero⟩
haveI : ∀ i : ι, _root_.Finite <| ℤ ⧸ Submodule.span ℤ {p i ^ e i} := fun i =>
Finite.of_equiv _ (p i ^ e i).quotientSpanEquivZMod.symm.toEquiv
haveI : _root_.Finite (⨁ i, ℤ ⧸ (Submodule.span ℤ {p i ^ e i} : Submodule ℤ ℤ)) :=
Finite.of_equiv _ DFinsupp.equivFunOnFintype.symm
exact Finite.of_equiv _ l.symm.toEquiv
