# mathlib3documentation

group_theory.finite_abelian

# Structure of finite(ly generated) abelian groups #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

• add_comm_group.equiv_free_prod_direct_sum_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.
• add_comm_group.equiv_direct_sum_zmod_of_fintype : 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) [ M] [ M] (hM : M) :
theorem add_comm_group.equiv_free_prod_direct_sum_zmod (G : Type u) [hG : add_group.fg G] :
(n : ) (ι : Type) [_inst_2 : fintype ι] (p : ι ) [_inst_3 : (i : ι), nat.prime (p i)] (e : ι ), nonempty (G ≃+ (fin n →₀ ) × (λ (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 add_comm_group.equiv_direct_sum_zmod_of_fintype (G : Type u) [finite G] :
(ι : Type) [_inst_3 : fintype ι] (p : ι ) [_inst_4 : (i : ι), nat.prime (p i)] (e : ι ), nonempty (G ≃+ (λ (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.