Module

IsSmallHilbertClassField.lean

Nyll.ClassFieldTheory.Definitions.FrobeniusAndHilbertClassFields.IsSmallHilbertClassField

1 declaration indexed from sourceView source ↗

Module documentation

Imports2

Imported by14

def

ClassFieldTheory.IsSmallHilbertClassField

Documentation

A small Hilbert class field is an everywhere-unramified finite abelian extension containing every other such extension.

Source context 2 commands

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

namespace ClassFieldTheory
universe u

Lean source · statement

def IsSmallHilbertClassField
    {K : Type u} [Field K] [NumberField K]
    (E : FiniteAbelianExtension K) : Prop