Module

SmallHilbertClassFieldLeBig.lean

Nyll.ClassFieldTheory.Theorems.FrobeniusAndHilbertClassFields.SmallHilbertClassFieldLeBig

1 declaration indexed from sourceView source ↗

Module documentation

The small Hilbert class field is a subfield of the big one

The extensions are intermediate fields of one separable closure, so the result is literal containment, not only an abstract embedding.

Imports2

Imported by1

Nyll.ClassFieldTheory.Theorems.FrobeniusAndHilbertClassFields.All

theorem

smallHilbertClassField_le_big

L25 ↗

ClassFieldTheory.smallHilbertClassField_le_big

Documentation

Every small Hilbert class field is contained in every big Hilbert class field inside the fixed separable closure.

Source context 3 commands

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

noncomputable section
namespace ClassFieldTheory
universe u

Lean source · statement

theorem smallHilbertClassField_le_big
    (K : Type u) [Field K] [NumberField K]
    (E F : FiniteAbelianExtension K)
    (hE : IsSmallHilbertClassField E)
    (hF : IsBigHilbertClassField F) :
    E.1 ≤ F.1

Module documentation

The small Hilbert class field is a subfield of the big one

Declarations

smallHilbertClassField_le_big