Module

IsFieldNorm.lean

Nyll.ClassFieldTheory.Definitions.LocalClassFieldTheory.IsFieldNorm

1 declaration indexed from sourceView source ↗

Module documentation

Imports1

Imported by7

def

ClassFieldTheory.IsFieldNorm

Documentation

A nonzero element of K is a field norm from L.

Source context 3 commands

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

noncomputable section
namespace ClassFieldTheory
universe u v

Lean source · statement

def IsFieldNorm
    (K : Type u) (L : Type v)
    [Field K] [Field L] [Algebra K L] [FiniteDimensional K L]
    (x : Kˣ) : Prop