LemmaStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-07-31

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.

In $(\mathbb{Z}/p)^\times$ , inversion pairs every class except $[1]_p$ and $[-1]_p$ , which are the only self-inverse classes

Statement

Let $p$ be prime. In the finite unit group $(\mathbb Z/p)^\times$ , inversion partitions all classes other than $[1]_p$ and $[-1]_p$ into disjoint pairs $\{u,u^{-1}\}$ with distinct members. The only self-inverse classes are $[1]_p$ and $[-1]_p$ .

When $p=2$ these two displayed classes coincide, and the unit group has that single element.

Facts & Assumptions

Given: A prime $p$ and the unit group $(\mathbb Z/p)^\times$ .

[L1]

The quotient $\mathbb Z/p$ is a field (For every prime $p$ , the two operations on $\mathbb{Z}/p$ make it a field).

[L2]

Units form a finite group under multiplication and every class has one standard representative; moreover $[a]_p=[b]_p$ exactly when $a\equiv b\pmod p$ , which means $p\mid(a-b)$ (The unit group $(\mathbb{Z}/n)^\times$ and Euler's totient $\varphi(n)=\lvert(\mathbb{Z}/n)^\times\rvert$ for $n\ge1$ , For $n\ge 1$ , every class in $\mathbb{Z}/n$ has one representative $r$ with $0\le r<n$ , so $\lvert\mathbb{Z}/n\rvert=n$ ; while $\mathbb{Z}/0$ is in bijection with $\mathbb{Z}$ , The congruence class $[a]_n$ and the quotient set $\mathbb{Z}/n$ , Congruence modulo an integer: $a\equiv b\pmod n$ when $n\mid(a-b)$ , including the moduli $0$ and $1$ ).

[L3]

An invertible element has a unique inverse, and every one-sided inverse equals that inverse (In a monoid, a left inverse and a right inverse of the same element are equal; hence an invertible element has exactly one inverse, and it is two-sided).

Proof

technique · direct

1.1

If a unit $u$ is self-inverse, then $u^2=[1]_p$ , so $(u-[1]_p)(u+[1]_p)=[0]_p$ . In a field a product is zero only if a factor is zero: if the first factor is nonzero, multiply by its inverse. Hence $u=[1]_p$ or $u=-[1]_p=[-1]_p$ .

1.2

Conversely, $[1]_p^2=[1]_p$ and $[-1]_p^2=[1]_p$ , so both displayed classes are self-inverse.

1.3

If $p=2$ , then $2\mid(1-(-1))$ , so $[1]_2=[-1]_2$ ; the unique nonzero standard class is $[1]_2$ , and it is the only unit.

L1L2

2.1

On the remaining finite set, inversion has no fixed point by steps 1.1 and 1.2. Since $u$ is an inverse of $u^{-1}$ , uniqueness in [L3] gives $(u^{-1})^{-1}=u$ . Therefore the inversion orbits are disjoint pairs $\{u,u^{-1}\}$ with distinct members.

step 1.1step 1.2L2L3

3.1

Steps 1.1 through 2.1 prove the pairing and its boundary case.

step 1.1step 1.2step 2.1step 1.3∎

Depends on

Used by

Wilson's theorem: for every prime p, (p-1)!≡-1pmod p Theorem

Dependency tree · next 3 levels

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

Mathematics LibreTexts, Wilson's Theorem (standard reference, not scraped)

In (Z/p)×(\mathbb{Z}/p)^\times(Z/p)×, inversion pairs every class except [1]p[1]_p[1]p​ and [−1]p[-1]_p[−1]p​, which are the only self-inverse classes