The Leopoldt defect of a CM field equals that of its maximal real subfield

Proved

Leopoldt.defect_eq_defect_maximalRealSubfield

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

leopoldtnumber-theory

Let $p$ be a prime and let $\mathbb{K}$ be a CM field with maximal totally real subfield $\mathbb{K}^+$ . Then the Leopoldt defects agree:

\mathcal{D}_L(\mathbb{K}) = \mathcal{D}_L(\mathbb{K}^+),

where $\mathcal{D}_L(\mathbb{L}) = \mathbb{Z}\text{-rk}\,E(\mathbb{L}) - \mathbb{Z}_p\text{-rk}\,\overline{E}(\mathbb{L})$ is the difference between the Dirichlet unit rank and the $\mathbb{Z}_p$ -rank of the $p$ -adic closure of the global units in the semilocal units at $p$ . The reason is that $E(\mathbb{K}^+)$ has finite index in $E(\mathbb{K})$ (the unit ranks agree), so the $\mathbb{Z}_p$ -ranks of the closures agree as well. No parity assumption on $p$ is needed.

Preamble

import Definitions.Def_LeopoldtDefect

open NumberField

Formal statement

namespace Leopoldt
theorem defect_eq_defect_maximalRealSubfield (p : ℕ) [Fact p.Prime]
    (K : Type*) [Field K] [NumberField K] [IsCMField K] :
    defect p K = defect p (maximalRealSubfield K) := by sorry
end Leopoldt

Source

P. Mihăilescu, On CM Z_p-extensions and the Leopoldt conjecture for CM fields, arXiv:1105.4544, §1.1, p.4 ("For CM extensions K, the contraposition of the conjecture herewith reduces to ... K⁺"); uses IsCMField.units_rank_eq_units_rank (rk E(K) = rk E(K⁺)).

View graph