Leopoldt's conjecture for CM fields with a biquadratic maximal real subfield

Proved

Leopoldt.leopoldt_CM_of_biquadratic_maximalRealSubfield

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

number-theoryp-adicunits

Let $K$ be a CM number field whose maximal totally real subfield $K^+$ is a biquadratic extension of $\mathbb Q$ : it is Galois of degree four and every automorphism has order at most two. Then Leopoldt’s conjecture holds for $K$ at every prime $p$ , including $2$ . This applies to certain non-Galois CM fields of degree eight, as well as abelian examples. The conjecture for a CM field is equivalent to that for its maximal real subfield, where the proved biquadratic case applies.

Preamble

import Definitions.Def_LeopoldtDefect
open NumberField

Formal statement

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

Source

Direct consequence of the platform theorems Leopoldt.leopoldtConjecture_iff_maximalRealSubfield and Leopoldt.leopoldt_totallyReal_biquadratic; CM descent of Leopoldt defect follows the basic setup of 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