Existing in Mathlib · Number theory

Dirichlet's Theorem on Primes in Arithmetic Progressions

Fix a positive modulus q and an invertible residue a modulo q. Infinitely many natural-number primes leave residue a when divided by q.

Dirichlet's theorem
primes in arithmetic progressions
invertible residue classes
Dirichlet characters
L-series
von Mangoldt function

Exact theorem

Exact Mathlib statement

theorem Nat.infinite_setOf_prime_and_eq_mod {q : ℕ} [NeZero q] {a : ZMod q} (ha : IsUnit a) : {p : ℕ | p.Prime ∧ (p : ZMod q) = a}.Infinite

The theorem at a glance

Dirichlet's Theorem — infinitely many primes in every unit residue class

A visual guide to the theorem's hypotheses, structure, and conclusion; the exact statement gives the formal detail.

An ivory analytic-number-theory poster connects a highlighted unit residue class to character waves, an L-series pole at one, a divergent prime contribution, and an unending prime progression. — A character decomposition and nonvanishing argument force the prime contribution in every invertible residue class to diverge, hence the class contains infinitely many primes.

Accessible poster text

Read the headline and panel text

ANALYTIC NUMBER THEORY · PRIMES IN PROGRESSIONS

DIRICHLET'S THEOREM

q ≥ 1 and a is a unit modulo q

{p ∈ ℕ | p is prime and p ≡ a (mod q)} is infinite

EVERY INVERTIBLE RESIDUE CLASS CONTAINS INFINITELY MANY PRIMES

HOW THE CHECKED ROUTE MOVES

1 · Isolate one residue class with the von Mangoldt function

2 · Decompose the class using Dirichlet characters

3 · Identify its L-series with logarithmic derivatives

4 · Cancel the pole at s = 1

5 · Use nonvanishing to control the remaining analytic term

6 · Remove the summable nonprime contribution

7 · A divergent prime contribution forces infinitely many primes

EXACT SCOPE

Infinitude only. No density, asymptotic count, least-prime bound, or claim for a nonunit residue class.

The detailed visual description covers the diagram and its local mathematical labels.

Statement structure

Statement and scope

Read the exact Mathlib declaration

This map summarizes the statement's structure; the exact Mathlib declaration remains authoritative.

An irregular procession of faceted prime tokens repeatedly enters one highlighted lane of a modular residue wheel and continues beyond the frame. — For every unit residue modulo a positive modulus, the primes returning to that class never run out.

Why it matters

A mathematical landmark

Dirichlet's theorem is a foundational bridge between prime-number distribution, harmonic analysis on residue classes, and complex analytic L-functions. The Mathlib file retains a substantial source-visible route from character orthogonality and nonvanishing to the exact infinitude conclusion.

ProofAtlas record

What has been checked

Upstream indexedPinned source bytes verified locally

Locally reproducedExact upstream declaration replayed

Reviewed pageCurrent public presentation reviewed

Accepted Atlas resultNot recorded for the preferred artifact

Mathlib is the source of the theorem; the local Lean replay and page review are separate.

Claim boundary

No new theorem is claimed

This target indexes Mathlib's infinitude theorem for primes in one invertible residue class modulo a nonzero natural modulus. It asserts infinitely many such primes; it does not give their density, an asymptotic counting formula, a least-prime bound, or a new proof.

The selected declaration proves infinitude, not equidistribution or a prime-counting asymptotic.
The residue class must be a unit modulo the nonzero modulus.
The theorem gives no explicit bound for the least or next prime in the class.
ProofAtlas is indexing an existing Mathlib theorem, not claiming new mathematics.

Source and local evidence

Where the theorem comes from

Existing declaration: Nat.infinite_setOf_prime_and_eq_mod in mathlib
Relationship: The checked artifact is the upstream declaration itself
Local Lean evidence: artifact.library.mathlib.dirichlet-primes-arithmetic-progressions.v001
Source: Open the pinned upstream reference