The cycle pattern of σ_p equals the decomposition type of f mod p

Proved

ChebotarevDensity.cyclePattern_eq_decompositionType

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

algebraic-number-theorynumber-theory

Let $f\in\mathbb Z[X]$ be monic with discriminant $\Delta(f)\neq0$ , with splitting field $K$ and Galois group $G$ , and let $p$ be a prime with $p\nmid\Delta(f)$ . If $\sigma\in G$ is a Frobenius substitution of $p$ , then the cycle pattern of $\sigma$ as a permutation of the zeros of $f$ equals the decomposition type of $f$ modulo $p$ :

\text{cycle pattern of }\sigma_p\;=\;\text{decomposition type of } f \bmod p .

Combined with Chebotarëv's theorem this yields Frobenius's theorem.

Preamble

import Definitions.Def_ChebotarevDensity_Defs

open Polynomial NumberField

Formal statement

namespace ChebotarevDensity

theorem cyclePattern_eq_decompositionType (f : ℤ[X]) (hf : f.Monic) (hdisc : f.discr ≠ 0)
    (p : ℕ) [Fact p.Prime] (hpd : ¬ (p : ℤ) ∣ f.discr) (σ : GalGroup f)
    (hσ : IsFrobeniusAt f p σ) :
    cyclePattern f σ = decompositionType f 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. 33: "Therefore, the cycle pattern of Frob_φ is indeed equal to the decomposition type of f modulo p."

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 $f\in\mathbb Z[X]$ that is monic with $\Delta(f)\neq0$ , every prime $p$ (typeclass fact) with $p\nmid\Delta(f)$ in $\mathbb Z$ , and every $\sigma\in G_f$ such that $\mathrm{IsFrobeniusAt}(f,p,\sigma)$ holds (some prime ideal $\mathfrak Q\ni p$ of $\mathcal O_{K_f}$ with $\sigma(x)\equiv x^{p}\bmod\mathfrak Q$ for all $x\in\mathcal O_{K_f}$ ): the multiset of cycle lengths (fixed points included) of the permutation that $\sigma$ induces on the distinct complex roots of $f$ equals the multiset of degrees of the monic irreducible factors of $f\bmod p$ in $\mathbb F_p[X]$ , counted with multiplicity.

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