Module

IsEverywhereUnramified.lean

Nyll.ClassFieldTheory.Definitions.FrobeniusAndHilbertClassFields.IsEverywhereUnramified

1 declaration indexed from sourceView source ↗

Module documentation

Imports2

Imported by3

def

ClassFieldTheory.IsEverywhereUnramified

Documentation

A number-field extension is unramified at all finite and infinite places.

Source context 2 commands

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

namespace ClassFieldTheory
universe u v

Lean source · statement

def IsEverywhereUnramified
    (K : Type u) (L : Type v)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L] : Prop