ClassFieldTheory.IsEverywhereLocalNorm
A unit is an everywhere local norm if it is a determinant norm after base change to every finite and every infinite completion of K.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
namespace ClassFieldTheory
universe u vLean source · statement
def IsEverywhereLocalNorm
(K : Type u) (L : Type v)
[Field K] [NumberField K]
[Field L] [Algebra K L] [FiniteDimensional K L]
(x : Kˣ) : Prop