Natural numbers in the residue field of an adic valuation ring

Let R be a Dedekind domain with fraction field K, and let v be a height one prime of R. The valuation ring of K at v is a local ring whose residue field has the same characteristic as R ⧸ v: a natural number vanishes in it exactly when its image in R lies in v.

Main results

• IsDedekindDomain.HeightOneSpectrum.natCast_residueField_valuationSubring_eq_zero_iff: a natural number is zero in the residue field of the valuation ring of K at v exactly when it lies in v.

theorem IsDedekindDomain.HeightOneSpectrum.natCast_residueField_valuationSubring_eq_zero_iff {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (n : ℕ) : ↑n = 0 ↔ ↑n ∈ v.asIdeal

A natural number is zero in the residue field of the valuation ring of K at v exactly when its image in R lies in v.