Module

FieldNormQuotient.lean

Nyll.ClassFieldTheory.Definitions.LocalClassFieldTheory.FieldNormQuotient

1 declaration indexed from sourceView source ↗

Module documentation

The field-norm quotient

Imports2

Nyll.ClassFieldTheory.Definitions.LocalClassFieldTheory.FieldNormSubgroup
Mathlib.GroupTheory.QuotientGroup.Basic

Imported by5

abbrev

FieldNormQuotient

ClassFieldTheory.FieldNormQuotient

Documentation

The norm quotient Kˣ / N_{L/K}(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

abbrev FieldNormQuotient
    (K : Type u) (L : Type v)
    [Field K] [Field L] [Algebra K L] [FiniteDimensional K L]