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

If a finite $p$ -group $P$ acts on a finite set $X$ , then $|X|\equiv|X^P|\pmod p$

Statement

If a finite $p$ -group $P$ acts on a finite set $X$ , then

$|X|\equiv|X^P|\pmod p.$

Facts & Assumptions

Given: A finite $p$ -group $P$ acting on a finite set $X$ .

[L1]

A finite $p$ -group has prime-power order (A finite $p$ -group has order $p^n$ for a prime $p$ and some $n\in\mathbb N$ ).

[L2]

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

[L3]

The $P$ -orbits partition $X$ (The orbits of a group action are the equivalence classes of $x\sim y$ iff $y=g\cdot x$ for some $g$ , and hence partition the acted-on set).

[L4]

[L5]

Every subgroup of $P$ has prime-power order (Every subgroup of a finite $p$ -group has order a power of $p$ ).

[L6]

The congruence $a\equiv b\pmod p$ means that $p$ divides $a-b$ (Congruence modulo an integer: $a\equiv b\pmod n$ when $n\mid(a-b)$ , including the moduli $0$ and $1$ ).

[L7]

A finite partition has total cardinality equal to the sum of its block cardinalities (The sum rule: a finite disjoint union is finite with $\lvert A \cup B\rvert = \lvert A\rvert + \lvert B\rvert$ and $\lvert\bigcup_{i \in I} A_i\rvert = \sum_{i \in I}\lvert A_i\rvert$ , and a sum over a finite index set splits along a partition).

[L8]

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 · direct

1.1

By [L3], $X$ is the disjoint union of its $P$ -orbits. An orbit is a singleton exactly when its point is fixed by every element of $P$ , so the singleton orbits are indexed by $X^P$ .

L2L3

1.2

For a non-singleton orbit $P\cdot x$ , the stabilizer $P_x$ is proper. By [L1], [L4], and [L5], its index is a positive power of $p$ , so $p$ divides $|P\cdot x|$ .

L1L4L5

2.1

Applying [L7] and [L8] to the orbit partition, every non-singleton orbit contributes a multiple of $p$ and the singleton orbits contribute $|X^P|$ . Thus $p$ divides $|X|-|X^P|$ , which is the asserted congruence by [L6].

step 1.1step 1.2L6L7L8∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 116 results over 25 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

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

If a finite ppp-group PPP acts on a finite set XXX, then ∣X∣≡∣XP∣(modp)|X|\equiv|X^P|\pmod p∣X∣≡∣XP∣(modp)