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

A finite $p$ -group action on $X$ has a global fixed point whenever $p\nmid|X|$

Statement

Let a finite $p$ -group $P$ act on a finite set $X$ . If $p\nmid|X|$ , then $X^P\ne\varnothing$ ; equivalently, the action has a point fixed by every element of $P$ .

Facts & Assumptions

Given: A finite $p$ -group $P$ acting on a finite set $X$ , with $p\nmid|X|$ .

[L1]

The fixed-point congruence gives $|X|\equiv|X^P|\pmod p$ (If a finite $p$ -group $P$ acts on a finite set $X$ , then $|X|\equiv|X^P|\pmod p$ ).

[L2]

The set $X^P$ consists of the points fixed by every element of $P$ (The fixed-point sets $X^g$ and $X^G$ of a group action).

[L3]

Congruence modulo $p$ means divisibility of the difference by $p$ (Congruence modulo an integer: $a\equiv b\pmod n$ when $n\mid(a-b)$ , including the moduli $0$ and $1$ ).

[L4]

A prime is positive and greater than $1$ (Prime and composite integers: $p$ is prime when $p > 1$ and its only positive divisors are $1$ and $p$ ).

Proof

technique · contradiction

1.1

Suppose, for contradiction, that $X^P=\varnothing$ . Then $|X^P|=0$ .

assume-contraL2

2.1

By [L1] and [L3], $p$ divides $|X|-|X^P|=|X|$ , contradicting the hypothesis.

step 1.1L1L3

3.1

Therefore $X^P$ is nonempty, and any of its elements is a global fixed point by [L2].

step 2.1L2L4discharge-contradiction∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 75 results over 20 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, Corollary 4.2 (standard reference, not scraped)

A finite ppp-group action on XXX has a global fixed point whenever p∤∣X∣p\nmid|X|p∤∣X∣