Theorems · Definition · commutative algebra

IsDedekindDomain.HeightOneSpectrum.intValuationDef

{R : Type u_1} →
  [inst : CommRing R] → [IsDedekindDomain R] → IsDedekindDomain.HeightOneSpectrum R → R → WithZero (Multiplicative ℤ)

The additive v-adic valuation of r : R is the exponent of v in the factorization of the ideal (r), if r is nonzero, or infinity, if r = 0. intValuationDef is the corresponding multiplicative valuation.

Defined in

Mathlib.RingTheory.DedekindDomain.AdicValuation

Cited by

9 results in Mathlib

Foundations

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

Assumes

CommRingIsDedekindDomain