CorollaryStatement: 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.

Orbit-stabiliser cardinality: $∣ G \cdot x ∣ = [G : G_{x}]$ whenever either side is finite, and $∣ G ∣ = ∣ G_{x} ∣ ∣ G \cdot x ∣$ for finite $G$

Statement

For an action of $G$ on $X$ and $x \in X$ ,

$∣ G \cdot x ∣ = [G : G_{x}]$

whenever either side is finite. In particular, if $G$ is finite, then

$∣ G ∣ = ∣ G_{x} ∣ ∣ G \cdot x ∣ .$

Facts & Assumptions

Given: A left action of $G$ on $X$ and a point $x \in X$ .

[L1]

The map $G / G_{x} \to G \cdot x$ , $g G_{x} \mapsto g \cdot x$ , is a bijection (Orbit-stabiliser: $G / G_{x} \to G \cdot x$ , $g G_{x} \mapsto g \cdot x$ , is a well-defined bijection).

[L2]

The index is the finite cardinality $[G : H] = ∣ G / H ∣$ when the coset set is finite (The coset set $G / H$ and the index $[G : H]$ of a subgroup).

[L3]

Finite cardinality is preserved by a bijection (The cardinality $∣ A ∣$ of a finite set).

[L4]

If $G$ is finite and $H \leq G$ , then $∣ G ∣ = [G : H] ∣ H ∣$ (Lagrange's theorem: $∣ G ∣ = [G : H] ∣ H ∣$ for every subgroup $H$ of a finite group $G$ ).

Proof

technique · direct

1.1

By [L1], the sets $G / G_{x}$ and $G \cdot x$ are bijective; [L2] and [L3] therefore give $∣ G \cdot x ∣ = ∣ G / G_{x} ∣ = [G : G_{x}]$ whenever they are finite.

L1L2L3

2.1

If $G$ is finite, [L4] applied to $G_{x} \leq G$ gives $∣ G ∣ = [G : G_{x}] ∣ G_{x} ∣ = ∣ G \cdot x ∣ ∣ G_{x} ∣$ .

step 1.1L4algebra∎

Depends on

Used by

Dependency tree · two levels

24 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

T. W. Judson, Abstract Algebra: Theory and Applications, 14.1, Theorem 14.11 (standard reference, not scraped)

Orbit-stabiliser cardinality: ∣G⋅x∣=[G:Gx]∣G⋅x∣=[G:Gx​] whenever either side is finite, and ∣G∣=∣Gx∣ ∣G⋅x∣∣G∣=∣Gx​∣∣G⋅x∣ for finite GG