NYLL
Module

KroneckerWeber.lean

Nyll.ClassFieldTheory.Theorems.KroneckerWeber
1 declaration indexed from sourceView source ↗

Module documentation

Kronecker--Weber theorem

Let L be a number field that is finite abelian over ℚ. Kronecker--Weber asserts that L is contained in a cyclotomic extension: there is a positive integer n and a ℚ-algebra embedding of L into ℚ(ζₙ). The positivity condition excludes the degenerate order-zero cyclotomic construction.

Imports4
Imported by1

Declarations

theorem

kroneckerWeber

L27 ↗
ClassFieldTheory.kroneckerWeber
Documentation

Kronecker--Weber. Every finite abelian extension of ℚ embeds in a cyclotomic field of positive order.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ClassFieldTheory
universe u
Lean source · statement
theorem kroneckerWeber
    (L : Type u) [Field L] [NumberField L] [IsAbelianGalois ℚ L] :
    ∃ n : ℕ, 0 < n ∧
      Nonempty (L →ₐ[ℚ] CyclotomicField n ℚ)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.