Cyclotomic Fields

Cyclotomic fields: roots of unity z^n = 1 mod m, primitive roots, and their connection to CRT decomposition. The Galois group Gal(Q(zeta_n)/Q) is isomorphic to (Z/nZ)^times.

Cyclotomic Fields

Summary

Cyclotomic fields: roots of unity z^n = 1 mod m, primitive roots, and their connection to CRT decomposition. The Galois group Gal(Q(zeta_n)/Q) is isomorphic to (Z/nZ)^times.

Statement

%
\label{def:cyclotomic-field}
For $n \geq 1$, the \textbf{$n$-th cyclotomic field} is:
\[
    \boxed{%
    \mathbb{Q}^\mathrm{cyc}_\tau(\zeta_n)
    := \mathbb{Q}_\tau(\zeta_n)
    = \biggl\{\sum_{j=0}^{d-1} a_j \zeta_n^j
    : a_j \in \mathbb{Q}_\tau\biggr\},}
\]
the smallest subfield of $\mathbb{C}_\tau$
containing $\mathbb{Q}_\tau$ and $\zeta_n$.
This is a finite extension of degree $\varphi(n)$,
with minimal polynomial the $n$-th \textbf{cyclotomic polynomial}:
\[
    \Phi_n(x) := \prod_{\substack{1 \leq k \leq n \\ \gcd(k,n) = 1}}
    (x - \zeta_n^k)
    \;\in\; \mathbb{Z}_\tau[x].
\]
The factorization $x^n - 1 = \prod_{d \mid n} \Phi_d(x)$
partitions all $n$-th roots by their primitive order.

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

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

Lean / Formalization Notes

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

Dependencies

• Canonical: I.D15, I.D19

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.