Module

SmallHilbertClassFieldUnique.lean

Nyll.ClassFieldTheory.Theorems.FrobeniusAndHilbertClassFields.SmallHilbertClassFieldUnique

1 declaration indexed from sourceView source ↗

Module documentation

Uniqueness of the small Hilbert class field inside a separable closure

The maximality condition determines an actual intermediate field, not merely an isomorphism class. It does not distinguish a unique field automorphism.

Imports1

Nyll.ClassFieldTheory.Definitions.FrobeniusAndHilbertClassFields.IsSmallHilbertClassField

Imported by2

theorem

smallHilbertClassFields_eq

L24 ↗

ClassFieldTheory.smallHilbertClassFields_eq

Documentation

Two small Hilbert class fields inside the same separable closure are equal as intermediate fields.

Source context 3 commands

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

noncomputable section
namespace ClassFieldTheory
universe u

Lean source · statement

theorem smallHilbertClassFields_eq
    (K : Type u) [Field K] [NumberField K]
    (E F : FiniteAbelianExtension K)
    (hE : IsSmallHilbertClassField E)
    (hF : IsSmallHilbertClassField F) :
    E.1 = F.1

Module documentation

Uniqueness of the small Hilbert class field inside a separable closure

Declarations

smallHilbertClassFields_eq