Leopoldt’s conjecture as equality of unit ranks

Proved

Leopoldt.leopoldtConjecture_iff_zpRankBelow_eq_units_rank

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

number-theoryp-adicunits

Let $p$ be prime and $K$ a number field. Write $r$ for the Dirichlet rank of the unit group, and $\bar E$ for the closure of its diagonal image in the semilocal units at $p$ . Then Leopoldt’s conjecture is equivalent to equality of ranks:

\mathcal D_L(K)=0\quad\Longleftrightarrow\quad \operatorname{rank}_{\mathbb Z_p}(\bar E)=r.

The mission’s bounded rank operation zpRankBelow measures the $p$ -adic rank of $\bar E$ using continuous embeddings of finite free $\mathbb Z_p$ modules, with the field degree as bound. The established upper bound ensures that defect zero forces equality, while equality immediately gives defect zero. This equivalence is a reusable interface between the defect formulation and a concrete rank goal.

Formalization Note The defect is natural-number subtraction; the rank upper bound is essential to the forward implication.

Preamble

import Definitions.Def_LeopoldtDefect

open NumberField

Formal statement

namespace Leopoldt
theorem leopoldtConjecture_iff_zpRankBelow_eq_units_rank (p : ℕ) [Fact p.Prime]
    (K : Type*) [Field K] [NumberField K] :
    LeopoldtConjecture p K ↔
      zpRankBelow p (Module.finrank ℚ K) (unitClosure p K) = Units.rank K := by sorry
end Leopoldt

Source

Preda Mihăilescu, On CM Z_p-extensions and the Leopoldt conjecture for CM fields, arXiv:1105.4544v4, Section 1.1, p. 3, definition of the Leopoldt defect as the difference of the integral rank of global units and the p-adic rank of their closure; combined with the established formalized rank upper bound Leopoldt.zpRankBelow_unitClosure_le_units_rank.

View graph