The Kronecker–Weber theorem

Every finite abelian extension of the rational numbers embeds into a cyclotomic field.

Roots of unity therefore suffice to generate fields containing every finite abelian extension of the rational numbers, and their union is the maximal abelian extension. This gives a concrete model for the broader problem of explicitly generating abelian extensions. As Milne recounts, Hilbert proved the theorem in 1896 after earlier incomplete proofs by Kronecker and Weber.

Lean code

`ClassFieldTheory.kroneckerWeber`

Published library source ↗Same source in NYLL ↗

theorem kroneckerWeber
    (L : Type u) [Field L] [NumberField L] [IsAbelianGalois ℚ L] :
    ∃ n : ℕ, 0 < n ∧
      Nonempty (L →ₐ[ℚ] CyclotomicField n ℚ)

In-scope Lean context

namespace ClassFieldTheory

universe u

Full declaration and proof

/-- **Kronecker--Weber.** Every finite abelian extension of `ℚ` embeds in a
cyclotomic field of positive order. -/
theorem kroneckerWeber
    (L : Type u) [Field L] [NumberField L] [IsAbelianGalois ℚ L] :
    ∃ n : ℕ, 0 < n ∧
      Nonempty (L →ₐ[ℚ] CyclotomicField n ℚ) := by
  let : Small.{0} L := numberField_small L
  let S := Shrink.{0} L
  let : NumberField S := numberField_shrink L
  let e : S ≃ₐ[ℚ] L := (Shrink.ringEquiv L).toRatAlgEquiv
  let : IsAbelianGalois ℚ S := by
    apply isAbelianGalois_of_equiv_equiv
      (f := RingEquiv.refl ℚ) (g := e.symm.toRingEquiv)
    apply RingHom.ext
    intro x
    change algebraMap ℚ S x = e.symm (algebraMap ℚ L x)
    exact (e.symm.commutes x).symm
  obtain ⟨n, hn, ⟨i⟩⟩ :=
    KroneckerWeber.exists_cyclotomicEmbedding S
  exact ⟨n, hn, ⟨i.comp e.symm.toAlgHom⟩⟩

Source credits and license

Copyright (c) 2026 Naganori Yamaguchi (https://github.com/n-yamaguchi-0729). All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Naganori Yamaguchi (assisted by OpenAI Codex)

The Kronecker–Weber theorem

Mathematical statement

Lean code

`ClassFieldTheory.kroneckerWeber`

References