LemmaStatement: Literature-sourcedProof: Literature-sourcedprecheck passjudge pass (deepseek-v4-pro + claude-sonnet-5)audited 2026-08-17

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 normal subgroup of a solvable group contains a nontrivial abelian subgroup normal in the whole group

Statement

Let $Q$ be a solvable group and let $N ⊴ Q$ with $N \neq 1$ . Then $N$ contains a subgroup $A \neq 1$ that is abelian and normal in $Q$ .

Facts & Assumptions

Given: A solvable group $Q$ and a normal subgroup $N ⊴ Q$ with $N \neq 1$ .

[L1]

The derived series of a group $N$ is $N^{(0)} = N$ , $N^{(r + 1)} = [N^{(r)}, N^{(r)}]$ ; $N$ is solvable when $N^{(n)} = 1$ for some $n \in N$ , and its derived length is the least such $n$ . The trivial group has derived length $0$ (The derived series, solvable groups, and derived length).

[L2]

Every subgroup and every quotient of a solvable group is solvable; no finiteness hypothesis is required (Subgroups and quotients of solvable groups are solvable).

[L3]

For every group $G$ , the derived subgroup $G^{'} = [G, G]$ is characteristic, hence normal (The derived subgroup is characteristic and the abelianization is universal).

[L4]

If $K char H$ and $H char G$ , then $K char G$ (Characteristic subgroups are normal, and characteristicity is transitive).

[L5]

If $K$ is characteristic in $N$ and $N ⊴ G$ , then $K ⊴ G$ (If $K$ is characteristic in $N$ and $N$ is normal in $G$ , then $K$ is normal in $G$ ).

[L6]

Let $N ⊴ G$ . Then $G / N$ is abelian if and only if $[G, G] \subseteq N$ ( $G / N$ is abelian if and only if $[G, G] \subseteq N$ ).

Proof

technique · direct

1.1L1L2given

$N$ is a subgroup of the solvable group $Q$ , so $N$ is solvable by [L2]. Let $n$ be its derived length, so $N^{(n)} = 1$ and $N^{(r)} \neq 1$ for $r < n$ by the leastness in [L1]. Since $N \neq 1$ and the trivial group is the only group of derived length $0$ , we have $n \geq 1$ .

2.1L1step 1.1

Put $A : = N^{(n - 1)}$ . Then $A \neq 1$ by the leastness in step 1.1, and $A \leq N$ because each term of the derived series lies in the preceding one by [L1].

2.2L1L6step 1.1

$[A, A] = N^{(n)} = 1$ by [L1] and step 1.1, so $A / 1$ is abelian by [L6] applied to the trivial normal subgroup of $A$ ; that is, $A$ is abelian.

3.1L1L3L4step 2.1

Each term of the derived series is characteristic in the preceding term by [L3], so iterating [L4] along $N^{(n - 1)} char \dots char N^{(0)} = N$ makes $A$ characteristic in $N$ .

4.1L5givenstep 2.1step 2.2step 3.1∎

$A$ is characteristic in $N$ and $N ⊴ Q$ , so $A ⊴ Q$ by [L5]. With steps 2.1 and 2.2, $A$ is a nontrivial abelian subgroup of $N$ that is normal in $Q$ . This proves the stated claim.

Depends on

Used by

Dependency tree · two levels

20 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

David A. Craven, Finite Group Theory, Theorem 2.13 (the claim opening its proof) (standard reference, not scraped)