NYLL
Module

SmallHilbertClassFieldExists.lean

Nyll.ClassFieldTheory.Theorems.FrobeniusAndHilbertClassFields.SmallHilbertClassFieldExists
1 declaration indexed from sourceView source ↗

Module documentation

Existence of the small Hilbert class field

The small Hilbert class field is characterized as an everywhere-unramified finite abelian extension containing every other such extension. In particular, real places are required to remain unramified.

Imports3
Imported by2

Declarations

theorem

exists_smallHilbertClassField

L24 ↗
ClassFieldTheory.exists_smallHilbertClassField
Documentation

A maximal everywhere-unramified finite abelian extension exists.

Source context 2 commands

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

open scoped NumberField
namespace ClassFieldTheory
Lean source · statement
theorem exists_smallHilbertClassField
    (K : Type) [Field K] [NumberField K] :
    ∃ E : FiniteAbelianExtension K, IsSmallHilbertClassField E

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