TheoremStatement: Literature-sourcedProof: Literature-sourcedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-13

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.

Every finite $p$ -group is nilpotent

Statement

Every finite $p$ -group is nilpotent. The trivial group is included and has nilpotency class zero.

Facts & Assumptions

Given: A prime $p$ and a finite group $G$ of order $p^{n}$ for some $n \in N$ .

[F1]

$Z_{r + 1} (G)$ is the inverse image of $Z (G / Z_{r} (G))$ under the quotient map (The upper central series).

[F2]

$G$ is nilpotent if $Z_{c} (G) = G$ for some $c$ ; the trivial group has class zero (Nilpotent groups and nilpotency class).

[L1]

Every nontrivial finite $p$ -group has nontrivial center (Every nontrivial finite $p$ -group has nontrivial center, in fact $p$ divides $∣ Z (P) ∣$ ).

[L2]

For $N ⊴ G$ , $∣ G / N ∣ = ∣ G ∣ / ∣ N ∣$ in the finite case (If $[G : N]$ is finite then $∣ G / N ∣ = [G : N]$ ; for finite $G$ this equals $∣ G ∣ / ∣ N ∣$ , Lagrange's theorem: $∣ G ∣ = [G : H] ∣ H ∣$ for every subgroup $H$ of a finite group $G$ ).

[L3]

Subgroups of $G / N$ correspond to subgroups of $G$ containing $N$ (Correspondence theorem: subgroups of $G / N$ correspond to subgroups of $G$ containing $N$ , with normality preserved).

Proof

technique · induction

1.1

If $n = 0$ , then $∣ G ∣ = 1$ , so $G = 1$ is nilpotent of class zero by [F2].

baseF2

1.2

Assume $n > 0$ and that every $p$ -group of order smaller than $p^{n}$ is nilpotent.

2.1

By [L1], $Z (G)$ is nontrivial. Its order is a positive power $p^{k}$ with $1 \leq k \leq n$ , and [L2] gives $∣ G / Z (G) ∣ = p^{n - k} < p^{n}$ .

step 1.2L1L2

3.1

By induction, $G / Z (G)$ is nilpotent, so its upper central series reaches the whole quotient at some term $c$ .

step 2.1ihF2

4.1

Starting with $Z_{1} (G) = Z (G)$ , [F1] shows inductively that the inverse image in $G$ of $Z_{r} (G / Z (G))$ is $Z_{r + 1} (G)$ . Since the quotient series reaches $G / Z (G)$ at $r = c$ , one has $Z_{c + 1} (G) = G$ .

step 3.1F1L3

5.1

Thus $G$ is nilpotent by [F2], completing the induction.

step 4.1F2discharge-induction∎

Depends on

Used by

Nilpotent groups, and in particular finite p-groups, are solvable Corollary

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 89 results over 18 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

J. S. Milne, Group Theory, Chapter 6 (standard reference, not scraped)
K. Conrad, Subgroup Series I (standard reference, not scraped)
K. Igusa, Notes on Jordan-Hölder, section 5 (standard reference, not scraped)

Every finite pp-group is nilpotent