Units at the height-one primes of ℚ

Let R be the ring of integers of ℚ in the sense of IsIntegralClosure R ℤ ℚ, and let v be a height-one prime of R, corresponding to the rational prime p = Rat.HeightOneSpectrum.primesEquiv v. This file compares the v-adic valuation with the p-adic valuation padicValRat p.

Main results

• Rat.HeightOneSpectrum.valuation_eq_one_iff_padicValRat_eq_zero: a nonzero rational number is a unit at v exactly when its p-adic valuation vanishes.

theorem Rat.HeightOneSpectrum.valuation_eq_one_iff_padicValRat_eq_zero {R : Type u_1} [CommRing R] [Algebra R ℚ] [IsIntegralClosure R ℤ ℚ] [IsDedekindDomain R] [IsFractionRing R ℚ] (v : IsDedekindDomain.HeightOneSpectrum R) {x : ℚ} (hx : x ≠ 0) : (IsDedekindDomain.HeightOneSpectrum.valuation ℚ v) x = 1 ↔ padicValRat (↑(primesEquiv v)) x = 0

A nonzero rational number is a unit at the height-one prime v exactly when its p-adic valuation vanishes, for p the rational prime corresponding to v.