LemmaStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-02

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 commutator subgroup is normal

Statement

For every group $G$ , its commutator subgroup $[G, G]$ is normal in $G$ .

Facts & Assumptions

Given: A group $G$ , its commutator subgroup $D = [G, G]$ , and an element $x \in G$ .

[F1]

The subgroup $D$ is generated by all elements $[g, h] = g h g^{- 1} h^{- 1}$ with $g, h \in G$ (Commutators $[g, h] = g h g^{- 1} h^{- 1}$ and the commutator subgroup $[G, G]$ ).

[L1]

The subgroup generated by a set is contained in every subgroup that contains that set (The subgroup $⟨ S ⟩$ generated by a subset, the cyclic subgroup $⟨ g ⟩$ , and cyclic groups).

[F2]

Conjugating a subgroup by a fixed group element produces a subgroup (Subgroup).

[L2]

A subgroup $D \leq G$ is normal if $x D x^{- 1} \subseteq D$ for every $x \in G$ (Equivalent characterisations of a normal subgroup by conjugates and left and right cosets).

Proof

technique · direct

1.1

Direct multiplication gives $x [g, h] x^{- 1} = [x g x^{- 1}, x h x^{- 1}]$ for all $g, h \in G$ .

F1algebra

1.2

The conjugate $x^{- 1} D x = {x^{- 1} d x : d \in D}$ is a subgroup of $G$ .

F2algebra

2.1

For every commutator $c = [g, h]$ , step 1.1 gives $x c x^{- 1} \in D$ , so $c \in x^{- 1} D x$ . Thus the subgroup $x^{- 1} D x$ contains every generator of $D$ , and [L1] gives $D \subseteq x^{- 1} D x$ .

step 1.1step 1.2F1L1

3.1

Conjugating the containment in step 2.1 by $x$ gives $x D x^{- 1} \subseteq D$ . Since $x$ was arbitrary, [L2] gives $D ⊴ G$ .

step 2.1L2algebra∎

Depends on

Used by

[Sₙ,Sₙ]=Aₙ for n≥2, and [Aₙ,Aₙ]=Aₙ for n≥5 Corollary
The abelianisation Gᵃᵇ:=G/[G,G] and its canonical map Definition
Φ(P)=P'Pᵖ for a finite p-group Theorem

Dependency tree · two levels

11 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

Encyclopedia of Mathematics, Commutator subgroup (standard reference, not scraped)