Fundamental_Theorem_of_Finite_Abelian_Groups
Provedabelian-groupsfinite-groupsfundamental-theoremgroup-theoryproofwiki
Every finite abelian group is an internal group direct product of cyclic groups whose orders are prime powers. The number of terms in the product and the orders of the cyclic groups are uniquely determined by the group.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Fundamental_Theorem_of_Finite_Abelian_Groups {G : Type _} [CommGroup G] [Fintype G] : ∃ (n : ℕ) (l : Fin n → ℕ), (∀ i, 1 < l i) ∧ Fintype.card G = Finset.prod Finset.univ l := by sorrySource