LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-16

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.

For odd prime $p$ , $p ∤ u$ , and $k \geq 1$ , the class of $1 + p u$ has order $p^{k - 1}$ modulo $p^{k}$

Statement

Let $p$ be an odd prime and $u \in Z$ with $p ∤ u$ . For every $k \geq 1$ , the class of $1 + p u$ in $(Z / p^{k})^{\times}$ has order $p^{k - 1}$ .

Facts & Assumptions

Given: An odd prime $p$ , an integer $u$ not divisible by $p$ , and $k \geq 1$ .

[L1]

The units modulo a positive modulus form a finite group (The unit group $(Z / n)^{\times}$ and Euler's totient $φ (n) = ∣ (Z / n)^{\times} ∣$ for $n \geq 1$ ), and a class is a unit exactly when its representative is coprime to the modulus (For $n \geq 1$ , $[a]_{n}$ is a unit if and only if $\gcd (a, n) = 1$ ).

[L2]

If $p ∤ v$ and $s \geq 1$ , then $(1 + p^{s} v)^{p} \equiv 1 + p^{s + 1} v (m o d p^{s + 2})$ (For odd prime $p$ and $s \geq 1$ , $(1 + p^{s} u)^{p} \equiv 1 + p^{s + 1} u (m o d p^{s + 2})$ ).

[L3]

Group powers satisfy $(x^{r})^{s} = x^{r s}$ (Exponent laws in a group: $g^{m + n} = g^{m} g^{n}$ and $(g^{m})^{n} = g^{m n}$ for all $m, n \in Z$ , and $(g h)^{n} = g^{n} h^{n}$ when $g$ and $h$ commute).

[L4]

$v_{p} (a) = j$ means $p^{j} ∣ a$ but $p^{j + 1} ∤ a$ (For a prime $p$ and a nonzero integer $a$ : $p^{v_{p} (a)} ∣ a$ and $p^{v_{p} (a) + 1} ∤ a$ ; $p^{k} ∣ a$ holds exactly for $k \leq v_{p} (a)$ ; $v_{p} (a) \geq 1$ exactly when $p ∣ a$ ; $v_{p} (1) = v_{p} (- 1) = 0$ ; and $v_{p} (p) = 1$ ), and valuations add on nonzero products ( $v_{p} (a b) = v_{p} (a) + v_{p} (b)$ for nonzero integers $a, b$ , and $v_{p} (a + b) \geq \min {v_{p} (a), v_{p} (b)}$ whenever $a$ , $b$ and $a + b$ are all nonzero).

[L5]

Mathematical induction holds on $N$ (The principle of mathematical induction).

[L6]

If an element has finite order $r$ , its $m$ th power is the identity exactly when $r ∣ m$ (If $ord (g) = n$ then $g^{k} = e$ iff $k$ is an integer multiple of $n$ , the powers $g^{0}, \dots, g^{n - 1}$ are distinct, and $⟨ g ⟩$ has exactly $n$ elements; if $g$ has infinite order then $g^{j} = g^{k}$ only for $j = k$ ).

Proof

technique · induction

1.1basegivenL4

For $j = 0$ , $(1 + p u)^{p^{0}} - 1 = p u$ has valuation $1$ .

1.2ihL2L3L4

Assume $(1 + p u)^{p^{j}} = 1 + p^{j + 1} v$ with $p ∤ v$ . Applying [L2] with $s = j + 1$ and using [L3] gives $(1 + p u)^{p^{j + 1}} = 1 + p^{j + 2} v^{'}$ with $p ∤ v^{'}$ .

1.3givenL1algebra

Any common prime divisor of $1 + p u$ and $p^{k}$ would be $p$ , but $1 + p u \equiv 1 (m o d p)$ . Thus $1 + p u$ is coprime to $p^{k}$ , so [L1] places its class in $(Z / p^{k})^{\times}$ .

2.1step 1.1step 1.2L5

By induction, $v_{p} ((1 + p u)^{p^{j}} - 1) = j + 1$ for every $j \geq 0$ .

3.1step 1.3step 2.1L4L6discharge-induction∎

By step 1.3 the order is defined in the finite unit group. Step 2.1 at $j = k - 1$ and [L6] show that it divides $p^{k - 1}$ . If it were a proper divisor of this prime power, it would divide $p^{k - 2}$ when $k \geq 2$ , so [L6] would make the $p^{k - 2}$ nd power equal to $1$ , contradicting step 2.1 at $j = k - 2$ ; for $k = 1$ the class is already the identity and has order $1$ .

Depends on

Used by

Dependency tree · two levels

59 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

Peter Hackman, Elementary Number Theory, §C.IV (standard reference, not scraped)

For odd prime pp, p∤up∤u, and k≥1k≥1, the class of 1+pu1+pu has order pk−1pk−1 modulo pkpk