Module

FieldNormSubgroup.lean

Nyll.ClassFieldTheory.Definitions.LocalClassFieldTheory.FieldNormSubgroup

1 declaration indexed from sourceView source ↗

Module documentation

Imports1

Imported by15

def

ClassFieldTheory.fieldNormSubgroup

Documentation

The subgroup N_{L/K}(Lˣ) of nonzero field norms.

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