Unit rank of quadratic fields

Proved

DirichletUnitTheorem.quadratic_unit_rank

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

algebraic-number-theorynumber-theory

Let $K$ be a quadratic number field, $[K:\mathbb Q]=2$ . Then

the unit rank of $K$ is $1$ if and only if $K$ is a real quadratic field (both embeddings are real), and
the unit rank of $K$ is $0$ if and only if $K$ is an imaginary quadratic field (no embedding is real).

For real quadratic fields this is the theory of Pell's equation.

Formalization Note "Real quadratic" is encoded as Mathlib's IsTotallyReal and "imaginary quadratic" as IsTotallyComplex; for degree $2$ these agree with the usual notions.

Preamble

import Mathlib
open NumberField

Formal statement

namespace DirichletUnitTheorem

theorem quadratic_unit_rank (K : Type*) [Field K] [NumberField K]
    (hK : Module.finrank ℚ K = 2) :
    (Module.rank ℤ (Additive (𝓞 K)ˣ) = 1 ↔ IsTotallyReal K) ∧
      (Module.rank ℤ (Additive (𝓞 K)ˣ) = 0 ↔ IsTotallyComplex K) := by sorry

end DirichletUnitTheorem

Source

Wikipedia, "Dirichlet's unit theorem" (article supplied by the account owner as a PDF), lead section ("if K is a quadratic field, the rank is 1 if it is a real quadratic field, and 0 if an imaginary quadratic field").

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. Let $K$ be a number field with $[K:\mathbb Q]=2$ . Then both of the following hold:

the rank of $\mathcal O_K^\times$ (a cardinal) equals $1$ if and only if $K$ is totally real (every infinite place of $K$ is real);
the rank of $\mathcal O_K^\times$ equals $0$ if and only if $K$ is totally complex (every infinite place of $K$ is complex).

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