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

The unit group modulo $n$ is the product of its odd-prime cyclic factors and its explicit $2$ -power factor

Statement

Let $n \geq 1$ have prime-power factorisation $n = 2^{a} \prod_{i < r} p_{i}^{k_{i}}$ , where the $p_{i}$ are distinct odd primes and $k_{i} \geq 1$ . Then

$(Z / n)^{\times} ≅ U_{2, a} \times \prod_{i < r} C_{p_{i}^{k_{i} - 1} (p_{i} - 1)},$

where $U_{2, 0}$ and $U_{2, 1}$ are trivial, $U_{2, 2} = C_{2}$ , and

$U_{2, a} = C_{2} \times C_{2^{a - 2}} (a \geq 3) .$

For $n = 1$ the product is empty and hence trivial.

Facts & Assumptions

Given: A positive integer $n$ and its displayed prime-power factorisation.

[L1]

CRT gives an isomorphism from a unit group to the product of the unit groups of pairwise coprime factors (For pairwise coprime positive moduli, the Chinese remainder bijection restricts to an isomorphism of unit groups).

[L2]

For odd $p$ , $(Z / p^{k})^{\times}$ is cyclic of order $p^{k - 1} (p - 1)$ (For every odd prime $p$ and $k \geq 1$ , $(Z / p^{k} Z)^{\times}$ is cyclic of order $p^{k - 1} (p - 1)$ ).

[L3]

For $a \geq 3$ , $(Z / 2^{a})^{\times} ≅ C_{2} \times C_{2^{a - 2}}$ (For $k \geq 3$ , $(Z / 2^{k} Z)^{\times} ≅ C_{2} \times C_{2^{k - 2}}$ , generated uniquely as $(- 1)^{ε} 5^{j}$ ).

[L4]

Given an injective list of primes containing every prime divisor of $n \geq 1$ , one has $n = \prod_{i} p_{i}^{v_{p_{i}} (n)}$ , the exponents being determined by $n$ (For $n \geq 1$ and any injective list $p : r \to Z$ of primes containing every prime divisor of $n$ , one has $n = \prod_{i < r} p_{i}^{v_{p_{i}} (n)}$ ; the exponents are determined by $n$ , and $v_{q} (n) = 0$ for every prime $q$ outside the list). The Given of this theorem supplies exactly such a list, namely the primes of the displayed factorisation.

[L5]

$φ (2) = 1$ and $φ (4) = 2$ by the prime-power formula (For a prime $p$ and $k \geq 1$ , $φ (p^{k}) = p^{k} - p^{k - 1}$ ).

[L7]

The totient is the cardinality of the unit group: $φ (n) = ∣ (Z / n)^{\times} ∣$ (The unit group $(Z / n)^{\times}$ and Euler's totient $φ (n) = ∣ (Z / n)^{\times} ∣$ for $n \geq 1$ ).

[L6]

Every group of prime order is cyclic (A finite group of prime order is cyclic and every nonidentity element generates it).

Proof

technique · direct

1.1

By [L4], the displayed factors are pairwise coprime, so [L1] decomposes the unit group into its $2$ -power factor and the odd-prime-power factors.

L4L1

2.1

Substitute [L2] for every odd factor and [L3] for the $2$ -power factor when $a \geq 3$ .

step 1.1L2L3

2.2

If $a = 0$ there is no $2$ -factor. If $a = 1$ , then [L5] gives $φ (2) = 1$ and [L7] reads that as $∣ (Z / 2)^{\times} ∣ = 1$ , so the unit group is trivial. If $a = 2$ , then [L5] and [L7] give $∣ (Z / 4)^{\times} ∣ = 2$ , prime order, so [L6] makes it cyclic.

step 1.1L5L6L7

3.1

Steps 2.1 and 2.2 give the asserted decomposition. When $n = 1$ , [L1] identifies the empty product with the one-element unit group.

step 2.1step 2.2L1∎

Depends on

Used by

Dependency tree · next 3 levels

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

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

The unit group modulo nn is the product of its odd-prime cyclic factors and its explicit 22-power factor