Theorems · Theorem · group theory

AddCommGroup.equiv_directSum_zmod_of_finite

∀ (G : Type u) [inst : AddCommGroup G] [Finite G],
  ∃ ι x p, ∃ (_ : ∀ (i : ι), Nat.Prime (p i)), ∃ e, Nonempty (G ≃+ DirectSum ι fun 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.

Defined in

Mathlib.GroupTheory.FiniteAbelian.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

AddCommGroupFinite