mathlib3 documentation

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.

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.

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.