Theorems · Definition · number theory

NumberField.HeightOneSpectrum.adicAbv

(K : Type u_1) →
  [inst : Field K] →
    {R : Type u_2} →
      [inst_1 : CommRing R] →
        [inst_2 : Algebra R K] →
          [IsDedekindDomain R] →
            [IsFractionRing R K] →
              IsDedekindDomain.HeightOneSpectrum R → [Module.Finite ℤ R] → [Module.Free ℤ R] → AbsoluteValue K ℝ

The v-adic absolute value on K defined as the norm of v raised to negative v-adic valuation

Defined in

Mathlib.NumberTheory.NumberField.Completion.FinitePlace

Cited by

21 results in Mathlib

Foundations

Depth 161 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldCommRingAlgebraIsDedekindDomainIsFractionRingModule.FiniteModule.Free