Unit rank of a totally real field: $r = [K:\mathbb{Q}] - 1$

Proved

Leopoldt.units_rank_of_isTotallyReal

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

leopoldtnumber-theory

Let $K$ be a totally real number field. Then its unit group $\mathcal{O}_K^\times$ has $\mathbb{Z}$ -rank

\operatorname{rk}_{\mathbb{Z}} \mathcal{O}_K^\times = [K:\mathbb{Q}] - 1.

This is Dirichlet's unit theorem $r = r_1 + r_2 - 1$ with $r_2 = 0$ and $r_1 = [K:\mathbb{Q}]$ .

Preamble

import Definitions.Def_LeopoldtDefect

open NumberField

Formal statement

namespace Leopoldt
theorem units_rank_of_isTotallyReal (K : Type*) [Field K] [NumberField K] [IsTotallyReal K] :
    Units.rank K = Module.finrank ℚ K - 1 := by sorry
end Leopoldt

Source

Dirichlet's unit theorem, e.g. J. Neukirch, Algebraic Number Theory, Chapter I, Theorem 7.4, specialised to r_2 = 0; used in arXiv:1105.4544 Section 1.1

View graph

Unit rank of a totally real field: r=[K:Q]−1r = [K:\mathbb{Q}] - 1r=[K:Q]−1

Unit rank of a totally real field: $r = [K:\mathbb{Q}] - 1$