Alphabeta MathThe Fundamental Theorem of Finite Abelian Groups
About this page
How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
✓ 19 results · all verified · 0 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 19 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.
1 · Prerequisites
Abstract Algebra
Number Theory
Real Analysis
2 · Logical flowchart
3 · Items
Definition
Internal direct products of finitely many normal subgroups
Theorem
Internal direct products are external direct products, equivalently every element has a unique factorisation
Definition
The p-primary component of an abelian group
Theorem
Cauchy's theorem for finite abelian groups
Theorem
A p-primary component has the full p-power order and is the unique subgroup of that order
Theorem
A finite abelian group is the internal direct product of its primary components
Lemma
A nontrivial finite abelian p-group with a unique subgroup of order p is cyclic
Theorem
A maximal-order cyclic subgroup splits off a finite abelian p-group
Theorem
Every finite abelian p-group is a direct product of cyclic p-groups
Definition
Elementary-divisor data for a finite abelian group
Lemma
The successive quotients pⁱG/pⁱ⁺¹G recover the cyclic summand multiplicities of a finite abelian p-group
Theorem
Fundamental theorem of finite abelian groups: elementary-divisor form
Definition
Invariant-factor data for a finite abelian group
Lemma
Elementary divisors regroup uniquely into invariant factors
Theorem
Fundamental theorem of finite abelian groups: invariant-factor form
Corollary
Converse of Lagrange for finite abelian groups: every divisor occurs as a subgroup order
Definition
The exponent of a finite group
Corollary
Invariant factors determine the order and exponent of a finite abelian group
Corollary
A nontrivial finite abelian group is cyclic if and only if it has one invariant factor
Definition
Indecomposable and decomposable nontrivial finite abelian groups
Theorem
Every nontrivial finite abelian group is an internal direct product of indecomposable subgroups
Corollary
The indecomposable finite abelian groups are exactly the nontrivial cyclic groups of prime-power order
Definition
Partitions of a positive integer
Corollary
Isomorphism classes of abelian groups of order pⁿ are counted by partitions of n
Corollary
The number of finite abelian groups of order n is the product of the partition numbers of the prime exponents of n
Definition
Squarefree positive integers
Corollary