Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-11
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 G be a nontrivial finite abelian p-group. If G has exactly one subgroup of order p, then G is cyclic.

Facts & Assumptions

Given: The objects and hypotheses in the statement.

[L1]

Let G be a finite abelian group and let p be a prime dividing ∣G∣. Then G contains an element, and hence a subgroup, of order p. (Cauchy's theorem for finite abelian groups).

[L2]

Let G be a group and let N⊴G be a normal subgroup (def-normal-subgroup). The quotient group, or factor group, G/N has the left cosets G/N:={gN:g∈G} as its elements (def-coset, def-index), with product (gN)(hN):=ghN. 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 G/N and coset product (gN)(hN)=ghN).

[L3]

If G is abelian and N⊴G, then G/N is abelian. (Every quotient group of an abelian group is abelian).

[L4]

Let N⊴G. If [G:N] is finite, then the quotient group G/N is finite and ∣G/N∣=[G:N]. In particular, if G is finite, then ∣G/N∣=∣G∣∣N∣. (If [G:N] is finite then ∣G/N∣=[G:N]; for finite G this equals ∣G∣/∣N∣).

[L5]

Let G be a group and g∈G, with integer powers as in def-group-power. Then ⟨g⟩  =  { gn  :  n∈Z }, the cyclic subgroup generated by g (def-generated-subgroup) being exactly the set of integer powers of g. Consequently every cyclic group is abelian, and so is every cyclic subgroup of any group. (⟨g⟩={ gn:n∈Z }, and every cyclic group is abelian).

[L6]

Let G be a group, g∈G, 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 ι:N→Z of lem-nat-embeds-int. Finite order. Suppose ord⁡(g)=n with n∈N, n≥1. Then: 1. for every k∈Z, gk=e if and only if k=qn for some q∈Z, that is, if and only if n∣k (thm-division-algorithm-in-z); 2. the powers g0,g1,…,gn−1 are pairwise distinct: if i,j∈N with i<n, j<n and gi=gj, then i=j; 3. ⟨g⟩={ gs:s∈N, s<n } and ⟨g⟩≈n; so ⟨g⟩ is finite with ∣⟨g⟩∣=n=ord⁡(g). Infinite order. If ord⁡(g)=∞ then for j,k∈Z, gj=gk implies j=k; so the integer powers of g are pairwise distinct and ⟨g⟩ is not finite. (If ord⁡(g)=n then gk=e iff k is an integer multiple of n, the powers g0,…,gn−1 are distinct, and ⟨g⟩ has exactly n elements; if g has infinite order then gj=gk only for j=k).

Proof

technique · contradiction
1.1

Assume for contradiction that G is not cyclic. Choose a∈G of maximal order pm and put A=⟨a⟩, which is then proper.

assume-contragivenL1L2L3L4L5L6
2.1

Cauchy's theorem in G/A gives b+A of order p. Thus pb=sa in additive notation for some integer s, while b∉A.

step 1.1
3.1

Maximality gives pmb=0, so pm−1sa=0. Since a has order pm, the integer s is divisible by p, say s=pt.

step 2.1
4.1

Then c=b−ta is nonzero, lies outside A, and satisfies pc=0. Its order-p subgroup differs from the unique order-p subgroup inside A, contradicting the hypothesis. Therefore G is cyclic.

step 3.1discharge-contradiction∎

Depends on

Used by

Dependency tree · two levels

37 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources