Module

IsUnramifiedAtFinitePlaces.lean

Nyll.ClassFieldTheory.Definitions.FrobeniusAndHilbertClassFields.IsUnramifiedAtFinitePlaces

1 declaration indexed from sourceView source ↗

Module documentation

Imports2

Imported by4

def

ClassFieldTheory.IsUnramifiedAtFinitePlaces

Documentation

A number-field extension is unramified at every finite prime of the base.

Source context 4 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
namespace ClassFieldTheory
universe u v

Lean source · statement

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