Theorems · Theorem · group theory

CommGroup.equiv_prod_multiplicative_zmod_of_finite

∀ (G : Type u_1) [inst : CommGroup G] [Finite G],
  ∃ ι x n, (∀ (i : ι), 1 < n i) ∧ Nonempty (G ≃* ((i : ι) → Multiplicative (ZMod (n i))))

The Structure Theorem For Finite Abelian Groups in a multiplicative version: A finite abelian group G is isomorphic to a finite product of finite cyclic groups.

Defined in

Mathlib.GroupTheory.FiniteAbelian.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommGroupFinite