mathlib documentation

group_theory.finite_abelian

Structure of finite(ly generated) abelian groups #

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.