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

Proved

Leopoldt.units_rank_of_isTotallyComplex

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

leopoldtnumber-theory

Let $K$ be a totally complex number field (for example a CM field). Then its unit group has $\mathbb{Z}$ -rank

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

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

Preamble

import Definitions.Def_LeopoldtDefect

open NumberField

Formal statement

namespace Leopoldt
theorem units_rank_of_isTotallyComplex (K : Type*) [Field K] [NumberField K]
    [IsTotallyComplex K] :
    Units.rank K = Module.finrank ℚ K / 2 - 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_1 = 0; used in arXiv:1105.4544 Section 1.1 for CM fields

View graph

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

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