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.

Every nontrivial finite $p$ -group has nontrivial center, in fact $p$ divides $|Z(P)|$

Statement

If $P$ is a nontrivial finite $p$ -group, then

$p\mid |Z(P)|.$

In particular, the center $Z(P)$ contains a nonidentity element.

Facts & Assumptions

Given: A nontrivial finite $p$ -group $P$ .

[L1]

Nontriviality means $|P|=p^n$ with $n\ge1$ (A finite $p$ -group has order $p^n$ for a prime $p$ and some $n\in\mathbb N$ ).

[L2]

For an action of $P$ on a finite set $X$ , $|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$ ).

[L3]

Conjugation gives a homomorphism $P\to\operatorname{Aut}(P)$ (The map $g\mapsto(x\mapsto gxg^{-1})$ is a homomorphism $G\to\operatorname{Aut}(G)$ with kernel $Z(G)$ and image $\operatorname{Inn}(G)$ ).

[L4]

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

[L5]

The center is the set of elements commuting with every element of $P$ (The center $Z(G)$ of a group).

[L6]

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$ ).

Proof

technique · direct

1.1

By [L3] and [L4], $P$ acts on itself by conjugation. An element is fixed by all conjugations exactly when it lies in $Z(P)$ by [L5].

L3L4L5

2.1

Applying [L2] to this action gives $|P|\equiv|Z(P)|\pmod p$ .

step 1.1L2

3.1

By [L1], $p$ divides $|P|$ . Hence [L6] and step 2.1 show that $p$ divides $|Z(P)|$ . Since $Z(P)$ contains the identity and its cardinality is a positive multiple of $p>1$ , it also contains a nonidentity element.

step 2.1L1L5L6algebra∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 82 results over 18 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 5.1 (standard reference, not scraped)
T. W. Judson, Abstract Algebra: Theory and Applications, 14.2 (standard reference, not scraped)

Every nontrivial finite ppp-group has nontrivial center, in fact ppp divides ∣Z(P)∣|Z(P)|∣Z(P)∣