NYLL
Module

CyclicHasseNormTheorem.lean

Nyll.ClassFieldTheory.Theorems.NormTheorems.CyclicHasseNormTheorem
1 declaration indexed from sourceView source ↗

Module documentation

The cyclic Hasse norm theorem

This module states the local-to-global norm principle for a finite cyclic Galois extension L / K of number fields. For a unit x of K, the conclusion identifies membership in the global field-norm subgroup with the condition of being a norm after base change to every finite and infinite completion of K.

Imports5
Imported by1

Declarations

theorem

cyclicHasseNormTheorem

L29 ↗
ClassFieldTheory.cyclicHasseNormTheorem
Documentation

For a finite cyclic number-field extension, a unit is a global norm if and only if it is a norm at every completion.

Source context 2 commands

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

open scoped NumberField
namespace ClassFieldTheory
Lean source · statement
theorem cyclicHasseNormTheorem
    (K L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
    (x : Kˣ) :
    IsFieldNorm K L x ↔ IsEverywhereLocalNorm K L x

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