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.

Jordan's derangement theorem: every transitive action of a finite group on a finite set with more than one element has a nonidentity element with no fixed points

Statement

Let a finite group $G$ act transitively on a finite set $X$ with $∣ X ∣ > 1$ . Then some nonidentity $g \in G$ is a derangement:

$X^{g} = \emptyset .$

Facts & Assumptions

Given: A transitive action of a finite group $G$ on a finite set $X$ with $∣ X ∣ > 1$ .

[L1]

A transitive action has exactly one orbit (Left group actions, transitive actions, and faithful actions).

[L2]

The fixed-point set is $X^{g} = {x : g \cdot x = x}$ (The fixed-point sets $X^{g}$ and $X^{G}$ of a group action).

[L3]

Cauchy-Frobenius gives $∣ G ∣ ∣ X / G ∣ = \sum_{g \in G} ∣ X^{g} ∣$ (Cauchy-Frobenius orbit counting: $∣ G ∣ ∣ X / G ∣ = \sum_{g \in G} ∣ X^{g} ∣$ for a finite group action).

[L4]

Finite cardinalities add over disjoint unions (The sum rule: a finite disjoint union is finite with $∣ A \cup B ∣ = ∣ A ∣ + ∣ B ∣$ and $∣ ⋃_{i \in I} A_{i} ∣ = \sum_{i \in I} ∣ A_{i} ∣$ , and a sum over a finite index set splits along a partition, The cardinality $∣ A ∣$ of a finite set).

[L5]

Finite sums over finite index sets are well-defined (The sum $\sum_{i \in S} a_{i}$ over a finite index set, and its product form).

Proof

technique · contradiction

1.1

By transitivity [L1], $∣ X / G ∣ = 1$ , so [L3] gives $\sum_{g \in G} ∣ X^{g} ∣ = ∣ G ∣$ .

L1L3

1.2

The identity fixes every point, so $∣ X^{e} ∣ = ∣ X ∣$ ; splitting its term from the finite sum gives $\sum_{g \in G} ∣ X^{g} ∣ = ∣ X ∣ + \sum_{g \neq e} ∣ X^{g} ∣$ .

L2L4L5

2.1

Suppose, for contradiction, that every nonidentity $g$ fixes a point. Then every term in the remaining sum is at least $1$ , so step 1.2 gives $\sum_{g} ∣ X^{g} ∣ \geq ∣ X ∣ + (∣ G ∣ - 1) > ∣ G ∣$ , since $∣ X ∣ > 1$ .

assume-contrastep 1.2L2L4L5

3.1

This contradicts step 1.1. Therefore some $g$ has $X^{g} = \emptyset$ ; the identity fixes all of $X$ , so this $g$ is nonidentity.

step 1.1step 2.1L2discharge-contradiction∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

29 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

K. Conrad, Group Actions, Theorem 6.6 (standard reference, not scraped)