Documentation

Atlas.NumberTheoryI.code.FinitePlaceAbsValue

source
noncomputable def FinitePlace.toAbsoluteValue {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) :
AbsoluteValue K ℝ
Instances For
    source
    theorem FinitePlace.toAbsoluteValue_isNontrivial {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) :
    (toAbsoluteValue v).IsNontrivial
    source
    theorem FinitePlace.toAbsoluteValue_pairwise_inequiv {K : Type u_1} [Field K] [NumberField K] (v₁ v₂ : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (h : v₁ ≠ v₂) :
    ¬(toAbsoluteValue v₁).IsEquiv (toAbsoluteValue v₂)