ClassFieldTheory.IsNormAtInfinitePlace
A unit of K is a norm at an infinite place w if its image in the completion 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
namespace ClassFieldTheory
universe u vLean source · statement
def IsNormAtInfinitePlace
(K : Type u) (L : Type v)
[Field K] [NumberField K]
[Field L] [Algebra K L] [FiniteDimensional K L]
(w : InfinitePlace K) (x : Kˣ) : Prop