English
A finite commutative group G is isomorphic to a finite product of finite cyclic groups.
Русский
Конечная коммутативная группа изоморфна конечному произведению циклических групп.
LaTeX
$$$\exists ι, \text{Fintype } ι, n: ι \to \mathbb{N},\ n(i)>1,\ G \cong_* (i\colon ι) \to Multiplicative(\mathbb{Z}/(n(i)))$$$
Lean4
/-- The **Structure Theorem For Finite Abelian Groups** in a multiplicative version:
A finite commutative group `G` is isomorphic to a finite product of finite cyclic groups. -/
theorem equiv_prod_multiplicative_zmod_of_finite (G : Type*) [CommGroup G] [Finite G] :
∃ (ι : Type) (_ : Fintype ι) (n : ι → ℕ),
(∀ (i : ι), 1 < n i) ∧ Nonempty (G ≃* ((i : ι) → Multiplicative (ZMod (n i)))) :=
by
obtain ⟨ι, inst, n, h₁, h₂⟩ := AddCommGroup.equiv_directSum_zmod_of_finite' (Additive G)
exact
⟨ι, inst, n, h₁,
⟨MulEquiv.toAdditive.symm <|
h₂.some.trans <| (DirectSum.addEquivProd _).trans (MulEquiv.piMultiplicative _).toAdditiveRight⟩⟩
