Structure of finite(ly generated) abelian groups

• AddCommGroup.equiv_free_prod_directSum_zmod : Any finitely generated abelian group is the product of a power of ℤ and a direct sum of some ZMod (p i ^ e i) for some prime powers p i ^ e i.
• CommGroup.equiv_free_prod_prod_multiplicative_zmod is a version for multiplicative groups.
• AddCommGroup.equiv_directSum_zmod_of_finite : Any finite abelian group is a direct sum of some ZMod (p i ^ e i) for some prime powers p i ^ e i.
• CommGroup.equiv_prod_multiplicative_zmod_of_finite is a version for multiplicative groups.

theorem Module.finite_of_fg_torsion (M : Type u) [AddCommGroup M] [Module ℤ M] [Module.Finite ℤ M] (hM : IsTorsion ℤ M) : Finite M

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

Structure theorem of finitely generated abelian groups : Any finitely generated abelian group is the product of a power of ℤ and a direct sum of some ZMod (p i ^ e i) for some prime powers p i ^ e i.

theorem AddCommGroup.equiv_directSum_zmod_of_finite (G : Type u) [AddCommGroup G] [Finite G] : ∃ (ι : Type) (x : Fintype ι) (p : ι → ℕ) (_ : ∀ (i : ι), Nat.Prime (p i)) (e : ι → ℕ), Nonempty (G ≃+ DirectSum ι fun (i : ι) => ZMod (p i ^ e i))

Structure theorem of finite abelian groups : Any finite abelian group is a direct sum of some ZMod (p i ^ e i) for some prime powers p i ^ e i.

theorem AddCommGroup.equiv_directSum_zmod_of_finite' (G : Type u_1) [AddCommGroup G] [Finite G] : ∃ (ι : Type) (x : Fintype ι) (n : ι → ℕ), (∀ (i : ι), 1 < n i) ∧ Nonempty (G ≃+ DirectSum ι fun (i : ι) => ZMod (n i))

Structure theorem of finite abelian groups : Any finite abelian group is a direct sum of some ZMod (n i) for some natural numbers n i > 1.

theorem AddCommGroup.finite_of_fg_torsion (G : Type u) [AddCommGroup G] [hG' : AddGroup.FG G] (hG : AddMonoid.IsTorsion G) : Finite G

theorem CommGroup.finite_of_fg_torsion (G : Type u) [CommGroup G] [Group.FG G] (hG : Monoid.IsTorsion G) : Finite G

theorem CommGroup.equiv_prod_multiplicative_zmod_of_finite (G : Type u_1) [CommGroup G] [Finite G] : ∃ (ι : Type) (x : Fintype ι) (n : ι → ℕ), (∀ (i : ι), 1 < n i) ∧ Nonempty (G ≃* ((i : ι) → Multiplicative (ZMod (n i))))

The Structure Theorem For Finite Abelian Groups in a multiplicative version: A finite commutative group G is isomorphic to a finite product of finite cyclic groups.

theorem CommGroup.equiv_free_prod_prod_multiplicative_zmod (G : Type u_1) [CommGroup G] [hG : Group.FG G] : ∃ (ι : Type) (j : Type) (x : Fintype ι) (x : Fintype j) (p : ι → ℕ) (_ : ∀ (i : ι), Nat.Prime (p i)) (e : ι → ℕ), Nonempty (G ≃* (j → Multiplicative ℤ) × ((i : ι) → Multiplicative (ZMod (p i ^ e i))))

The Structure theorem of finitely generated abelian groups in a multiplicative version : Any finitely generated abelian group is the product of a power of ℤ and a direct product of some ZMod (p i ^ e i) for some prime powers p i ^ e i.