Theorem of Dirichlet (analytic density of primes in arithmetic progressions)

Proved

ChebotarevDensity.dirichlet_density

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

algebraic-number-theorynumber-theory

Let $m$ be a positive integer and $a$ an integer with $\gcd(a,m)=1$ . Then the set of primes $p$ with $p\equiv a\pmod m$ has analytic (Dirichlet) density $1/\varphi(m)$ :

\lim_{s\to1^+}\frac{\sum_{p\equiv a\ (m)}p^{-s}}{\log\frac1{s-1}}=\frac1{\varphi(m)},

where $\varphi$ is Euler's totient function.

This is the case $f=X^m-1$ of Chebotarëv's theorem and the base case (cyclotomic extensions of $\mathbb Q$ ) of Chebotarëv's proof.

Preamble

import Definitions.Def_ChebotarevDensity_Defs

open Polynomial NumberField

Formal statement

namespace ChebotarevDensity

theorem dirichlet_density (m : ℕ) (hm : 0 < m) (a : ℤ) (ha : Int.gcd a m = 1) :
    HasDirichletDensity {p : ℕ | (p : ℤ) ≡ a [ZMOD m]} (1 / (Nat.totient m : ℝ)) := 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, pp. 30–31, "Theorem of Dirichlet" (with the definition of density given there)

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 number $m$ with $m>0$ and every integer $a$ with $\gcd(a,m)=1$ (gcd of $a$ and $m$ as integers, i.e. $\gcd(|a|,m)=1$ ): the set $S=\{p\in\mathbb N : p\equiv a \pmod m \text{ as integers}\}$ has analytic density $1/\varphi(m)$ , i.e.

\frac{\sum_{p\in S,\ p\text{ prime}}p^{-s}}{\log\big(1/(s-1)\big)}\longrightarrow\frac{1}{\varphi(m)}\qquad (s\to1,\ s>1),

where $\varphi$ is Euler's totient function and only primes of $S$ enter the sum (the set $S$ itself also contains non-primes, which are ignored by the definition). For $m=1$ the congruence is always true and the claimed density is $1$ .

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