Theorem of Frobenius (density of primes with a given decomposition type)

Proved

ChebotarevDensity.frobenius_density

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$ , and let $G$ be its Galois group, viewed as a group of permutations of the $n$ zeros of $f$ . Let $t$ be a partition of $n$ (a multiset of positive integers). Then the set of primes $p\nmid\Delta(f)$ for which $f \bmod p$ has decomposition type $t$ has analytic density

\frac{\#\{\sigma\in G:\ \sigma\text{ has cycle pattern } t\}}{\#G}.

In particular the primes modulo which $f$ splits into linear factors have density $1/\#G$ .

Formalization Note $t$ ranges over all multisets of natural numbers; if $t$ is not a partition of $n$ both the set and the count are empty and the density is $0$ .

Preamble

import Definitions.Def_ChebotarevDensity_Defs

open Polynomial NumberField

Formal statement

namespace ChebotarevDensity

theorem frobenius_density (f : ℤ[X]) (hf : f.Monic) (hdisc : f.discr ≠ 0) (t : Multiset ℕ) :
    HasDirichletDensity (decompositionTypeSet f t)
      ((Nat.card {σ : GalGroup f // cyclePattern f σ = t} : ℝ) / Nat.card (GalGroup f)) := 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, "Theorem of Frobenius"

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$ and every finite multiset $t$ of natural numbers: the set of primes $p$ with $p\nmid\Delta(f)$ whose decomposition type (multiset of degrees of monic irreducible factors of $f\bmod p$ , with multiplicity) equals $t$ has analytic density

\frac{\#\{\sigma\in G_f:\ \mathrm{cyclePattern}(f,\sigma)=t\}}{\#G_f},

where $\mathrm{cyclePattern}(f,\sigma)$ is the multiset of cycle lengths, fixed points included, of $\sigma$ acting on the distinct complex roots of $f$ , and cardinalities are Nat.card cast to $\mathbb R$ ( $G_f$ is finite and nonempty). Analytic density means $\big(\sum_{p} p^{-s}\big)/\log(1/(s-1))$ tends to that value as $s\to1^+$ .

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