English
Any finite abelian group is a finite direct sum of cyclic p-power groups.
Русский
Любая конечная абелева группа есть конечная прямая сумма циклических p-ограниченных групп.
LaTeX
$$$G$ конечная абелева группа; \exists ι, Fintype ι, p, e : ι \to \mathbb{N}, \, G \cong_+ \bigoplus_{i\in ι} \mathbb{Z}/p_i^{e_i}\mathbb{Z}$$$
Lean4
/-- **Structure theorem of finite abelian groups** : Any finite abelian group is a direct sum of
some `ZMod (n i)` for some natural numbers `n i > 1`. -/
theorem equiv_directSum_zmod_of_finite' (G : Type*) [AddCommGroup G] [Finite G] :
∃ (ι : Type) (_ : Fintype ι) (n : ι → ℕ), (∀ i, 1 < n i) ∧ Nonempty (G ≃+ ⨁ i, ZMod (n i)) := by
classical
obtain ⟨ι, hι, p, hp, n, ⟨e⟩⟩ := AddCommGroup.equiv_directSum_zmod_of_finite G
refine ⟨{ i : ι // n i ≠ 0 }, inferInstance, fun i ↦ p i ^ n i, ?_, ⟨e.trans (directSumNeZeroMulEquiv ι _ _).symm⟩⟩
rintro ⟨i, hi⟩
exact one_lt_pow₀ (hp _).one_lt hi
