Roots of Unity CRT Decomposition

CRT decomposition of roots of unity: for coprime moduli m1, m2, a root of unity mod m1*m2 decomposes into roots mod m1 and mod m2. Connects cyclotomic structure to the CRT basis that pervades the spectral theory.

Roots of Unity CRT Decomposition

Summary

CRT decomposition of roots of unity: for coprime moduli m1, m2, a root of unity mod m1*m2 decomposes into roots mod m1 and mod m2. Connects cyclotomic structure to the CRT basis that pervades the spectral theory.

Statement

%
\label{thm:primitive-roots}
A root $\zeta_n^k \in \mu_n$ is \textbf{primitive}
--- i.e., generates $\mu_n$ ---
if and only if $\gcd(k, n) = 1$.
For each $n \geq 1$,
the number of primitive $n$-th roots of unity
is $\varphi(n)$ (Euler's totient).

Proof / Justification

The element $\zeta_n^k$ generates $\mu_n$
iff the multiples $\{k, 2k, \ldots, nk\}$
cover all residue classes modulo $n$,
which holds precisely when $\gcd(k, n) = 1$.

Source Context

• Registry source: book-01.jsonl line 197
• Manuscript source: 2nd-edition/book-i-categorical-foundations/02_mainmatter/part17/ch79-cyclotomic-fields.tex lines 56-65

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookI.Boundary.Cyclotomic
• Name: Tau.Boundary.root_of_unity_crt

Dependencies

• Canonical: I.D88, I.D19

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.