Module

ComplexInfinitePlaceAllNorm.lean

Nyll.ClassFieldTheory.Theorems.NormTheorems.ComplexInfinitePlaceAllNorm

1 declaration indexed from sourceView source ↗

Module documentation

Norms at a complex infinite place

The positivity condition is vacuous at a complex place. Consequently every nonzero base-field element is a determinant norm from the whole archimedean tensor algebra.

Imports2

Imported by1

Nyll.ClassFieldTheory.Theorems.NormTheorems.All

theorem

isNormAtInfinitePlace_of_complex

L29 ↗

ClassFieldTheory.isNormAtInfinitePlace_of_complex

Documentation

The determinant norm from K_v ⊗_K L is surjective on the image of Kˣ when v is complex.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
namespace ClassFieldTheory
universe u v

Lean source · statement

theorem isNormAtInfinitePlace_of_complex
    (K : Type u) (L : Type v)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
    (v : InfinitePlace K) (hv : v.IsComplex) (x : Kˣ) :
    IsNormAtInfinitePlace K L v x

Module documentation

Norms at a complex infinite place

Declarations

isNormAtInfinitePlace_of_complex