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.
A nontrivial finite abelian p-group with a unique subgroup of order p is cyclic
Statement
Let be a nontrivial finite abelian -group. If has exactly one subgroup of order , then is cyclic.
Facts & Assumptions
Given: The objects and hypotheses in the statement.
Let be a finite abelian group and let be a prime dividing . Then contains an element, and hence a subgroup, of order . (Cauchy's theorem for finite abelian groups).
Let be a group and let be a normal subgroup (def-normal-subgroup). The quotient group, or factor group, has the left cosets as its elements (def-coset, def-index), with product Independence of the chosen representatives is proved in thm-coset-multiplication-well-defined-iff-normal, and the group axioms are proved in thm-quotient-group-laws. (The quotient group and coset product ).
If is abelian and , then is abelian. (Every quotient group of an abelian group is abelian).
Let . If is finite, then the quotient group is finite and In particular, if is finite, then (If is finite then ; for finite this equals ).
Let be a group and , with integer powers as in def-group-power. Then the cyclic subgroup generated by (def-generated-subgroup) being exactly the set of integer powers of . Consequently every cyclic group is abelian, and so is every cyclic subgroup of any group. (, and every cyclic group is abelian).
Let be a group, , and let orders be as in def-order-in-a-group. Throughout, a natural number written where an integer is expected means its image under the embedding of lem-nat-embeds-int. Finite order. Suppose with , . Then: 1. for every , if and only if for some , that is, if and only if (thm-division-algorithm-in-z); 2. the powers are pairwise distinct: if with , and , then ; 3. and ; so is finite with . Infinite order. If then for , implies ; so the integer powers of are pairwise distinct and is not finite. (If then iff is an integer multiple of , the powers are distinct, and has exactly elements; if has infinite order then only for ).
Proof
Assume for contradiction that is not cyclic. Choose of maximal order and put , which is then proper.
Cauchy's theorem in gives of order . Thus in additive notation for some integer , while .
Maximality gives , so . Since has order , the integer is divisible by , say .
Then is nonzero, lies outside , and satisfies . Its order- subgroup differs from the unique order- subgroup inside , contradicting the hypothesis. Therefore is cyclic.
Depends on
Cauchy's theorem for finite abelian groups
The quotient group and coset product
Every quotient group of an abelian group is abelian
If is finite then ; for finite this equals
, and every cyclic group is abelian
If then iff is an integer multiple of , the powers are distinct, and has exactly elements; if has infinite order then only for