Module

BigHilbertClassFieldExists.lean

Nyll.ClassFieldTheory.Theorems.FrobeniusAndHilbertClassFields.BigHilbertClassFieldExists

1 declaration indexed from sourceView source ↗

Module documentation

Existence of the big Hilbert class field

The big Hilbert class field is characterized intrinsically as a finite abelian extension unramified at every finite prime and containing every other finite abelian extension with that property. No particular field chosen by the implementation appears in the statement.

Imports3

Imported by2

theorem

exists_bigHilbertClassField

L25 ↗

ClassFieldTheory.exists_bigHilbertClassField

Documentation

A maximal finite-prime-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_bigHilbertClassField
    (K : Type) [Field K] [NumberField K] :
    ∃ E : FiniteAbelianExtension K, IsBigHilbertClassField E

Module documentation

Existence of the big Hilbert class field

Declarations

exists_bigHilbertClassField