LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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.

The centralizer of a normal subgroup is normal

Statement

If $N ⊴ G$ , then $C_{G} (N) ⊴ G$ .

Facts & Assumptions

Given: A group $G$ and a normal subgroup $N ⊴ G$ .

[L1]

$C_{G} (N) = {g \in G : g n = n g for every n \in N}$ , and it is a subgroup of $G$ (The centralizer $C_{G} (H)$ of a subgroup).

[L2]

$N ⊴ G$ means $g N g^{- 1} = N$ for every $g \in G$ (Normal subgroup: invariance under conjugation).

Proof

technique · direct

1.1

Fix $g \in G$ , $x \in C_{G} (N)$ and $n \in N$ . By [L2] the element $g^{- 1} n g$ lies in $N$ , so $x (g^{- 1} n g) = (g^{- 1} n g) x$ by [L1].

L1L2given

2.1

Multiplying that identity by $g$ on the left and by $g^{- 1}$ on the right gives $(g x g^{- 1}) n = g x (g^{- 1} n g) g^{- 1} = g (g^{- 1} n g) x g^{- 1} = n (g x g^{- 1})$ , and since $n \in N$ was arbitrary, $g x g^{- 1} \in C_{G} (N)$ by [L1].

L1step 1.1algebra

3.1

Hence $g C_{G} (N) g^{- 1} \subseteq C_{G} (N)$ for every $g \in G$ . Applying this inclusion to $g^{- 1}$ and conjugating by $g$ gives $C_{G} (N) \subseteq g C_{G} (N) g^{- 1}$ , so $g C_{G} (N) g^{- 1} = C_{G} (N)$ for every $g \in G$ , which is normality by [L2]. This proves the stated claim.

L1L2step 2.1∎

Depends on

Used by

Philip Hall: in a finite solvable group the Fitting subgroup contains its own centralizer Theorem

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 15 results over 12 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, Proposition 3.22 (standard reference, not scraped)