TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-11

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.

$G / C_{G} (x) \to {Cl}_{G} (x)$ is a bijection, so $∣ {Cl}_{G} (x) ∣ = [G : C_{G} (x)]$ whenever these cardinalities are finite

Statement

For a group $G$ and $x \in G$ , the map

$G / C_{G} (x) ⟶ {Cl}_{G} (x), g C_{G} (x) ⟼ g x g^{- 1},$

is a well-defined bijection. Consequently

$∣ {Cl}_{G} (x) ∣ = [G : C_{G} (x)]$

whenever these cardinalities are finite, in particular when $G$ is finite.

Facts & Assumptions

Given: A group $G$ and an element $x \in G$ .

[L1]

Orbit-stabiliser gives a bijection from the cosets of a point stabilizer to its orbit (Orbit-stabiliser: $G / G_{x} \to G \cdot x$ , $g G_{x} \mapsto g \cdot x$ , is a well-defined bijection).

[L2]

The finite cardinality of an orbit is the index of its stabilizer (Orbit-stabiliser cardinality: $∣ G \cdot x ∣ = [G : G_{x}]$ whenever either side is finite, and $∣ G ∣ = ∣ G_{x} ∣ ∣ G \cdot x ∣$ for finite $G$ ).

[L3]

The conjugacy class is ${Cl}_{G} (x) = {g x g^{- 1} : g \in G}$ and the centralizer is $C_{G} (x) = {g : g x g^{- 1} = x}$ (The conjugacy class ${Cl}_{G} (x)$ and centralizer $C_{G} (x)$ of an element).

[L4]

The centralizer $C_{G} (x)$ is a subgroup of $G$ ( $C_{G} (x)$ and $N_{G} (H)$ are subgroups of $G$ ).

[L5]

The maps $x \mapsto g x g^{- 1}$ form the conjugation homomorphism (The map $g \mapsto (x \mapsto g x g^{- 1})$ is a homomorphism $G \to Aut (G)$ with kernel $Z (G)$ and image $Inn (G)$ ).

[L6]

A homomorphism into a symmetric group defines a group action (Actions of $G$ on $X$ correspond exactly to homomorphisms $G \to Sym (X)$ ).

Proof

technique · direct

1.1

By [L5] and [L6], $G$ acts on itself by conjugation. By [L3], the orbit of $x$ is ${Cl}_{G} (x)$ and its stabilizer is $C_{G} (x)$ , which is a subgroup by [L4].

L3L4L5L6

2.1

Applying [L1] to this action gives the displayed well-defined bijection $g C_{G} (x) \mapsto g x g^{- 1}$ .

step 1.1L1

3.1

Applying [L2] to the same orbit gives $∣ {Cl}_{G} (x) ∣ = [G : C_{G} (x)]$ whenever finite.

step 1.1step 2.1L2∎

Depends on

Used by

Dependency tree · two levels

27 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

P. Brosnan, Undergraduate Algebra Notes, 3.14: G-Sets, Corollary 3.109 (standard reference, not scraped)
T. W. Judson, Abstract Algebra: Theory and Applications, 14.2 (standard reference, not scraped)

G/CG(x)→Cl⁡G(x)G/CG​(x)→ClG​(x) is a bijection, so ∣Cl⁡G(x)∣=[G:CG(x)]∣ClG​(x)∣=[G:CG​(x)] whenever these cardinalities are finite