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) [add_comm_group M] [module ℤ M] [module.finite ℤ M] (hM : module.is_torsion ℤ M) :

finite M

source

theorem add_comm_group.equiv_free_prod_direct_sum_zmod (G : Type u) [add_comm_group G] [hG : add_group.fg G] :

∃ (n : ℕ) (ι : Type) [_inst_2 : fintype ι] (p : ι → ℕ) [_inst_3 : ∀ (i : ι), nat.prime (p i)] (e : ι → ℕ), nonempty (G ≃+ (fin n →₀ ℤ) × direct_sum ι (λ (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.

source

theorem add_comm_group.equiv_direct_sum_zmod_of_fintype (G : Type u) [add_comm_group G] [finite G] :

∃ (ι : Type) [_inst_3 : fintype ι] (p : ι → ℕ) [_inst_4 : ∀ (i : ι), nat.prime (p i)] (e : ι → ℕ), nonempty (G ≃+ direct_sum ι (λ (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.

source

theorem add_comm_group.finite_of_fg_torsion (G : Type u) [add_comm_group G] [hG' : add_group.fg G] (hG : add_monoid.is_torsion G) :

finite G

source

theorem comm_group.finite_of_fg_torsion (G : Type u) [comm_group G] [group.fg G] (hG : monoid.is_torsion G) :

finite G