Leopoldt's conjecture for CM fields with multiquadratic maximal real subfield

Proved

Leopoldt.leopoldt_CM_of_multiquadratic_maximalRealSubfield

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

number-theoryp-adicunits

Let $K$ be a CM field whose maximal real subfield $K^+$ is multiquadratic over $\mathbb Q$ . Equivalently, $K^+/\mathbb Q$ is Galois and every automorphism squares to the identity. Then Leopoldt’s conjecture holds for $K$ at every prime $p$ . There is no need for $K/\mathbb Q$ itself to be Galois. The established multiquadratic theorem proves the conjecture for $K^+$ ; the established CM defect equivalence transfers it to $K$ .

Preamble

import Definitions.Def_LeopoldtDefect
open NumberField

Formal statement

namespace Leopoldt
theorem leopoldt_CM_of_multiquadratic_maximalRealSubfield (p : ℕ) [Fact p.Prime]
    (K : Type*) [Field K] [NumberField K] [IsCMField K]
    [IsGalois ℚ (maximalRealSubfield K)]
    (hG : ∀ σ : maximalRealSubfield K ≃ₐ[ℚ] maximalRealSubfield K, σ * σ = 1) :
    LeopoldtConjecture p K := by sorry
end Leopoldt

Source

Combination of platform theorems Leopoldt.leopoldtConjecture_iff_maximalRealSubfield and Leopoldt.leopoldt_totallyReal_multiquadratic; CM descent of Leopoldt defect in Preda Mihăilescu, On CM Z_p-extensions and the Leopoldt conjecture for CM fields, https://arxiv.org/abs/1105.4544, Section 1.1.

View graph