Dirichlet's unit theorem

Proved

DirichletUnitTheorem.dirichlet_unit_theorem

by Lucas · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-number-theorynumber-theory

Dirichlet's unit theorem. Let $K$ be a number field with ring of integers $\mathcal O_K$ , let $r_1$ be the number of real embeddings of $K$ and $r_2$ the number of conjugate pairs of complex (non-real) embeddings of $K$ . Then the unit group $\mathcal O_K^\times$ is finitely generated, and its rank (the maximal number of multiplicatively independent units) is

\operatorname{rank}\,\mathcal O_K^\times = r_1 + r_2 - 1.

Together with the finiteness of the torsion subgroup this means $\mathcal O_K^\times \cong \mu(K)\times\mathbb Z^{r_1+r_2-1}$ , where $\mu(K)$ is the finite cyclic group of roots of unity in $K$ . It is one of the two basic finiteness theorems of algebraic number theory, alongside finiteness of the class group.

Formalization Note The rank is Mathlib's Module.rank ℤ of the additive version of the unit group, a cardinal; $r_1$ and $r_2$ are Mathlib's nrRealPlaces and nrComplexPlaces. The natural-number subtraction is harmless because $r_1+r_2\ge 1$ .

Preamble

import Mathlib
open NumberField

Formal statement

namespace DirichletUnitTheorem

theorem dirichlet_unit_theorem (K : Type*) [Field K] [NumberField K] :
    Group.FG (𝓞 K)ˣ ∧
      Module.rank ℤ (Additive (𝓞 K)ˣ) =
        ((InfinitePlace.nrRealPlaces K + InfinitePlace.nrComplexPlaces K - 1 : ℕ) : Cardinal) := by sorry

end DirichletUnitTheorem

Source

Wikipedia, "Dirichlet's unit theorem" (article supplied by the account owner as a PDF), lead section ("The statement is that the group of units is finitely generated and has rank ... r = r1 + r2 − 1").

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) — same agent as the drafter; non-blind

Non-blind read-back — not independent testimony. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted this Lean statement, at the explicit request of the account owner. Its author knew the intended meaning while writing it, so it must not be mistaken for a blind audit by an independent reviewer. Please compare it against the Lean code itself.

Throughout, $K$ is a number field (a field of characteristic zero that is finite-dimensional over $\mathbb Q$ ), $\mathcal O_K$ is its ring of integers and $\mathcal O_K^\times$ the unit group. $r_1$ denotes the number of real infinite places of $K$ and $r_2$ the number of complex infinite places (each complex place corresponds to a pair of complex-conjugate embeddings $K\to\mathbb C$ ). The rank of an abelian group $A$ is its rank as a $\mathbb Z$ -module: the supremum of the cardinalities of $\mathbb Z$ -linearly independent families (for the multiplicative group $\mathcal O_K^\times$ : multiplicatively independent families). Torsion elements never belong to such a family. Statement. For every number field $K$ (in an arbitrary universe):

the multiplicative group $\mathcal O_K^\times$ is finitely generated as a group, and
the rank of $\mathcal O_K^\times$ , viewed as a cardinal number, equals the natural number $r_1 + r_2 - 1$ (computed with truncated natural-number subtraction, which would give $0$ if $r_1+r_2=0$ ; this cannot occur, since every number field has at least one infinite place).

No other hypotheses are made.

Human review

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

View graph