IsDedekindDomain.HeightOneSpectrum.valuationOfNeZeroToFun_eq

theorem IsDedekindDomain.HeightOneSpectrum.valuationOfNeZeroToFun_eq : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {K : Type v} [inst_2 : Field K] [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (x : Kˣ), ↑(v.valuationOfNeZeroToFun x) = v.valuation ↑x

This theorem states that for any integral domain `R` with the property of being a Dedekind domain, and any field of fractions `K` of `R`, if `v` is a height-one prime ideal spectrum of `R` and `x` is a unit of `K`, then the fraction field extension of the valuation of the non-zero element `x` mapped under `v` is equivalent to the valuation of `v` applied to the unit `x`. This means that the valuation process is consistent whether we consider the element as part of the integral domain or as part of its field of fractions.

More concisely: For any Dedekind domain `R` and its field of fractions `K`, if `v` is a height-1 prime ideal of `R`, and `x` is a unit in `K` mapping to `v` in `R`, then the valuation of `x` in `K` is equal to the valuation of `v(x)` in `R`.