Module

FieldNormHom.lean

Nyll.ClassFieldTheory.Definitions.LocalClassFieldTheory.FieldNormHom

1 declaration indexed from sourceView source ↗

Module documentation

Imports1

Imported by3

def

ClassFieldTheory.fieldNormHom

Documentation

The field norm as a homomorphism on multiplicative groups.

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 fieldNormHom
    (K : Type u) (L : Type v)
    [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] :
    Lˣ →* Kˣ