ClassFieldTheory.IsNormAtFinitePlace
A unit of K is a norm at a finite place w if its image in K_w is a determinant norm from K_w ⊗_K L.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
namespace ClassFieldTheory
universe u vLean source · statement
def IsNormAtFinitePlace
(K : Type u) (L : Type v)
[Field K] [NumberField K]
[Field L] [Algebra K L] [FiniteDimensional K L]
(w : HeightOneSpectrum (𝓞 K)) (x : Kˣ) : Prop