AddCommGroup.equiv_free_prod_directSum_zmod

theorem AddCommGroup.equiv_free_prod_directSum_zmod : ∀ (G : Type u) [inst : AddCommGroup G] [hG : AddGroup.FG G], ∃ n ι x p, ∃ (_ : ∀ (i : ι), (p i).Prime), ∃ e, Nonempty (G ≃+ (Fin n →₀ ℤ) × DirectSum ι fun i => ZMod (p i ^ e i))

The **Structure theorem of finitely generated abelian groups** states that any finitely generated abelian group `G` can be expressed as the product of a power of the integers `ℤ` and a direct sum of integers modulo a prime power `p i ^ e i` for some indices `i`. Specifically, for a given abelian group `G`, there exists a natural number `n`, a type `ι`, a function `x`, and a function `p` such that for each `i` in `ι`, `p i` is a prime, and there exists a function `e` such that there is a nonempty isomorphism between the group `G` and the product of the group of `n`-tuples of integers and the direct sum, over `i`, of the groups of integers modulo `p i ^ e i`.

More concisely: Every finitely generated abelian group is isomorphic to the direct product of a free abelian group and a finite direct sum of cyclic groups of prime power order.