The Leopoldt defect is invariant under isomorphism

Proved

Leopoldt.defect_congr

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

leopoldtnumber-theory

Let $p$ be a prime and let $K \cong L$ be isomorphic number fields. Then their Leopoldt defects at $p$ agree: $\mathcal{D}_L(K) = \mathcal{D}_L(L)$ . In particular Leopoldt's conjecture for a number field depends only on its isomorphism class.

Preamble

import Definitions.Def_LeopoldtDefect

open NumberField

Formal statement

namespace Leopoldt
theorem defect_congr (p : ℕ) [Fact p.Prime]
    {K L : Type*} [Field K] [NumberField K] [Field L] [NumberField L]
    (e : K ≃ₐ[ℚ] L) : defect p K = defect p L := by sorry
end Leopoldt

Source

P. Mihăilescu, On CM Z_p-extensions and the Leopoldt conjecture for CM fields, arXiv:1105.4544, §1, Remark 1.A (Leopoldt defect does not decrease in finite extensions); M. Laurent, Rang p-adique d'unités et action de groupes, J. reine angew. Math. 399 (1989), 81–108, Introduction. (Isomorphism invariance: apply Remark 1.A to the degree-one extensions L/K and K/L.)

View graph