Frobenius substitution in cyclotomic fields: σ_p(ζ) = ζ^p

Proved

ChebotarevDensity.cyclotomic_frobenius_eq_pow

by Lucas · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-number-theorynumber-theory

Let $m$ be a positive integer, let $K$ be the splitting field of $X^m-1$ over $\mathbb Q$ (the $m$ -th cyclotomic field) and $G$ its Galois group. Let $p$ be a prime not dividing $m$ , and let $\sigma\in G$ be a Frobenius substitution of $p$ . Then for every primitive $m$ -th root of unity $\zeta\in K$ ,

\sigma(\zeta)=\zeta^p .

In other words, under the isomorphism $G\cong(\mathbb Z/m\mathbb Z)^\times$ , the Frobenius substitution $\sigma_p$ is a well-defined element (not just a conjugacy class) and corresponds to $p \bmod m$ .

This identifies Dirichlet's theorem with the case $f=X^m-1$ of Chebotarëv's theorem.

Preamble

import Definitions.Def_ChebotarevDensity_Defs

open Polynomial NumberField

Formal statement

namespace ChebotarevDensity

theorem cyclotomic_frobenius_eq_pow (m : ℕ) (hm : 0 < m) (p : ℕ) (hp : p.Prime) (hpm : ¬ p ∣ m)
    (σ : GalGroup (X ^ m - 1)) (hσ : IsFrobeniusAt (X ^ m - 1) p σ)
    (ζ : SplitField (X ^ m - 1)) (hζ : IsPrimitiveRoot ζ m) :
    σ ζ = ζ ^ p := by sorry

end ChebotarevDensity

Source

P. Stevenhagen and H. W. Lenstra, Jr., "Chebotarëv and his density theorem", The Mathematical Intelligencer 18 (1996), no. 2, 26–37, https://doi.org/10.1007/BF03027290, p. 34: "if p is a prime number not dividing m, then the Frobenius substitution σ_p is the element of G that under the isomorphism G ≅ (Z/mZ)^* corresponds to (p mod m)"

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) - non-blind, same agent that drafted the statements

Non-blind read-back. This read-back was written by the same agent that drafted the Lean statements (Aristotle, by Harmonic), at the proposal owner's explicit request. It is not independent testimony: the author knew the intended meaning when writing it. Reviewers should compare it against the Lean code themselves rather than rely on it as a blind audit.

For every natural $m>0$ , every prime $p$ with $p\nmid m$ , every $\sigma$ in the Galois group $G$ of the splitting field $K$ of $X^m-1$ over $\mathbb Q$ (the polynomial $X^m-1$ taken in $\mathbb Z[X]$ and mapped to $\mathbb Q[X]$ ) such that $\mathrm{IsFrobeniusAt}(X^m-1,p,\sigma)$ holds (some prime ideal $\mathfrak Q\ni p$ of $\mathcal O_K$ with $\sigma(x)\equiv x^p\bmod\mathfrak Q$ for all $x\in\mathcal O_K$ ), and every $\zeta\in K$ that is a primitive $m$ -th root of unity: $\sigma(\zeta)=\zeta^{p}$ .

Human review

Endorsed by Shuze Chen · Oct 1, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph