NYLL
Module

FieldNormSubgroupIsOpen.lean

Nyll.ClassFieldTheory.Theorems.LocalClassFieldTheory.FieldNormSubgroupIsOpen
1 declaration indexed from sourceView source ↗

Module documentation

Openness of the local norm subgroup

For a finite abelian extension of a nonarchimedean local field, the subgroup of nonzero field norms is open in the multiplicative group of the base.

Imports4
Imported by1

Declarations

theorem

isOpen_fieldNormSubgroup

L22 ↗
ClassFieldTheory.isOpen_fieldNormSubgroup
Documentation

The norm subgroup of a finite abelian local extension is open.

Source context 1 command

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

namespace ClassFieldTheory
Lean source · statement
theorem isOpen_fieldNormSubgroup
    (K L : Type)
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] :
    IsOpen (fieldNormSubgroup K L : Set Kˣ)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.