DefinitionDefinition: Literature-sourcedProof: Not applicableSession-authored (Fable 5 assisted)judge pass (deepseek-v4-pro + gpt-5.6-terra)audited 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.

The derived series, solvable groups, and derived length

Definition

The derived series of a group $G$ is defined recursively by $G^{(0)} = G, G^{(r + 1)} = [G^{(r)}, G^{(r)}] .$ Each term is characteristic, hence normal, in the preceding term by The derived subgroup is characteristic and the abelianization is universal.

The group $G$ is solvable if $G^{(n)} = 1$ for some $n \in N$ . Its derived length is the least such $n$ . This least index exists because the set of terminating indices is a nonempty subset of $N$ and every such subset has a least element (The well-ordering principle). Thus the trivial group has derived length $0$ , and a nontrivial abelian group has derived length $1$ .

Depends on

Used by

Nilpotent groups, and in particular finite p-groups, are solvable Corollary
A composition series and the derived series of S₃ Example
Composition and derived series of S₄ Example
Every solvable group is abelian False statement
Homomorphisms respect commutator subgroups and derived series Lemma
A group is solvable if and only if it has a subnormal series with abelian factors Theorem
A₅ and Sₙ for n≥5 are not solvable Theorem
Extensions and finite direct products of solvable groups are solvable Theorem
Subgroups and quotients of solvable groups are solvable Theorem

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 39 results over 9 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)