Theorems · Theorem · group theory

AddCommGroup.equiv_free_prod_directSum_zmod

∀ (G : Type u) [inst : AddCommGroup G] [hG : AddGroup.FG G],
  ∃ n ι 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.

Defined in

Mathlib.GroupTheory.FiniteAbelian.Basic

Cited by

2 results in Mathlib

Foundations

Depth 160 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommGroupAddGroup.FG