Theorems · Definition · commutative algebra

IsDedekindDomain.HeightOneSpectrum.adicAbv

{R : Type u_1} →
  [inst : CommRing R] →
    [IsDedekindDomain R] →
      {K : Type u_2} →
        [inst_2 : Field K] →
          [inst_3 : Algebra R K] →
            [IsFractionRing R K] → IsDedekindDomain.HeightOneSpectrum R → {b : NNReal} → 1 < b → AbsoluteValue K ℝ

The v-adic absolute value on K defined as b raised to negative v-adic valuation, for some b in ℝ≥0

Defined in

Mathlib.RingTheory.DedekindDomain.AdicValuation

Cited by

6 results in Mathlib

Foundations

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

Assumes

CommRingIsDedekindDomainFieldAlgebraIsFractionRing