Multiquadratic fields embed in cyclotomic fields (Kronecker–Weber, exponent 2)

Proved

NumberField.exists_algHom_cyclotomicField_of_exponent_two

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

algebraic-number-theorycyclotomic-fieldsnumber-theory

Kronecker–Weber for multiquadratic fields. Let $K$ be a number field which is Galois over $\mathbb{Q}$ and whose Galois group $G = \mathrm{Gal}(K/\mathbb{Q})$ has exponent dividing $2$ , i.e. $\sigma^2 = 1$ for every $\sigma \in G$ (so $G \cong (\mathbb{Z}/2)^r$ and $K$ is a multiquadratic field $\mathbb{Q}(\sqrt{d_1},\dots,\sqrt{d_r})$ ). Then $K$ embeds into a cyclotomic field: there is an integer $n > 0$ and a $\mathbb{Q}$ -algebra homomorphism

K \hookrightarrow \mathbb{Q}(\zeta_n).

This is the exponent- $2$ case of the Kronecker–Weber theorem, which follows from Kummer theory over $\mathbb{Q}$ (such $K$ is generated by square roots of rationals) together with the fact that every rational number is a square in some cyclotomic field (quadratic Gauss sums and $\sqrt{2} = \zeta_8 + \zeta_8^{-1}$ ).

Preamble

import Mathlib.NumberTheory.Cyclotomic.Basic
import Mathlib.NumberTheory.NumberField.Basic
import Mathlib.FieldTheory.Galois.Basic

Formal statement

theorem NumberField.exists_algHom_cyclotomicField_of_exponent_two (K : Type*) [Field K]
    [NumberField K] [IsGalois ℚ K] (hK : ∀ σ : K ≃ₐ[ℚ] K, σ * σ = 1) :
    ∃ n : ℕ, 0 < n ∧ Nonempty (K →ₐ[ℚ] CyclotomicField n ℚ) := by sorry

Source

L. C. Washington, Introduction to Cyclotomic Fields (2nd ed., GTM 83), Chapter 14 (The Kronecker–Weber Theorem), Theorem 14.1; exponent-2 case via Kummer theory over Q and Gauss sums (Ch. 4, Lemma 4.8 / quadratic Gauss sum).

View graph