# 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.
• 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.
theorem Module.finite_of_fg_torsion (M : Type u) [] [] [] (hM : ) :
theorem AddCommGroup.equiv_free_prod_directSum_zmod (G : Type u) [] [hG : ] :
∃ (n : ) (ι : Type) (x : ) (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) [] [] :
∃ (ι : Type) (x : ) (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) [] [] :
∃ (ι : Type) (x : ) (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 (q i) for some prime powers q i > 1.

theorem AddCommGroup.finite_of_fg_torsion (G : Type u) [] [hG' : ] (hG : ) :
theorem CommGroup.finite_of_fg_torsion (G : Type u) [] [] (hG : ) :