Alphabeta Math
TheoremStatement: 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.

Cauchy's theorem for finite abelian groups

Statement

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.

Facts & Assumptions

Given: The objects and hypotheses in the statement.

[L1]

Let P be a property of naturals such that for every n∈N, if P(m) holds for all m<n then P(n). Then P(n) holds for all n∈N. (At n=0 the hypothesis is vacuous, so P(0) is forced.) (Strong (complete) induction).

[L2]

Let G be a finite group and H≤G. Then ∣G∣=[G:H] ∣H∣. Consequently, under the canonical embedding ι:N→Z, ∣H∣ divides ∣G∣. (Lagrange's theorem: ∣G∣=[G:H]∣H∣ for every subgroup H of a finite group G).

[L3]

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∣).

[L4]

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

[L5]

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).

[L6]

Let G be a finite group such that the positive integer ∣G∣ is prime. Then every g≠e has order ∣G∣, satisfies ⟨g⟩=G, and hence generates G. In particular, G is cyclic. (A finite group of prime order is cyclic and every nonidentity element generates it).

[L7]

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).

[L8]

If G=⟨g⟩ is cyclic, then exactly one of the following applies: - if g has infinite order, G≅(Z,+); - if g has finite order n, necessarily n≥1, then G≅(Z/n,+). (Every cyclic group is isomorphic to (Z,+) or to (Z/n,+) for its finite order n≥1).

Proof

technique · induction
1.1

For strong induction on ∣G∣, the trivial group has no relevant prime divisor, and if ∣G∣=p then G is cyclic of order p.

basegivenL1L2L3L4L5L6L7L8
2.1

Fix the induction hypothesis for every finite abelian group of order smaller than ∣G∣. Choose x≠e. If ⟨x⟩=G, cyclic-group classification supplies x∣G∣/p of order p. Otherwise put H=⟨x⟩, a nontrivial proper subgroup.

ihstep 1.1
3.1

If p∣∣H∣, the induction hypothesis in H gives an element of order p. If p∤∣H∣, then p∣∣G/H∣ and the induction hypothesis in the smaller finite abelian quotient gives a coset yH of order p.

step 2.1
4.1

In the latter case yp∈H. Let q be the order of yp; then q∣∣H∣ and p∤q. Since the coset of y has order p, the order of y is pq, so yq has order p.

step 3.1
5.1

Every branch supplies an element of order p, completing the strong induction.

step 4.1discharge-induction∎

Depends on

Used by

Dependency tree · two levels

49 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