NYLL
Module

MemFieldNormSubgroupIff.lean

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

Module documentation

Membership in the field-norm subgroup

This module gives the concrete meaning of the public predicate IsFieldNorm. For a finite-dimensional extension of fields L / K and a unit x of K, it states that x belongs to the range of the unit-valued field norm exactly when some unit of L has algebra norm equal to x. No Galois, local-field, or topological assumption is required.

Imports1
Imported by1

Declarations

theorem

mem_fieldNormSubgroup_iff

L27 ↗
ClassFieldTheory.mem_fieldNormSubgroup_iff
Documentation

Membership in the norm subgroup is equivalent to being the algebra norm of a unit of the extension field.

Source context 3 commands

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

noncomputable section
namespace ClassFieldTheory
universe u v
Lean source · statement
theorem mem_fieldNormSubgroup_iff
    (K : Type u) (L : Type v)
    [Field K] [Field L] [Algebra K L] [FiniteDimensional K L]
    (x : Kˣ) :
    IsFieldNorm K L x ↔
      ∃ y : Lˣ, Algebra.norm K (y : L) = (x : K)

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