Commit 2026-01-03 19:24 ba60f6ca

View on Github →

feat(RingTheory/DedekindDomain/AdicValuation): introduce intAdicAbv (#33324) We introduce

def intAdicAbvDef (r : R) : ℝ≥0 := toNNReal (ne_zero_of_lt hb) (v.intValuation r)

and the corresponding AbsoluteValue R ℝ.

Estimated changes

Modified Mathlib/RingTheory/DedekindDomain/AdicValuation.lean

modified def IsDedekindDomain.HeightOneSpectrum.adicAbv

modified def IsDedekindDomain.HeightOneSpectrum.adicAbvDef

modified theorem IsDedekindDomain.HeightOneSpectrum.adicAbv_coe_eq_one_iff

modified theorem IsDedekindDomain.HeightOneSpectrum.adicAbv_coe_le_one

modified theorem IsDedekindDomain.HeightOneSpectrum.adicAbv_coe_lt_one_iff

added theorem IsDedekindDomain.HeightOneSpectrum.adicAbv_of_algebraMap

added theorem IsDedekindDomain.HeightOneSpectrum.adicAbv_of_mk'

added def IsDedekindDomain.HeightOneSpectrum.intAdicAbv

added def IsDedekindDomain.HeightOneSpectrum.intAdicAbvDef

added theorem IsDedekindDomain.HeightOneSpectrum.intAdicAbv_eq_one_iff

added theorem IsDedekindDomain.HeightOneSpectrum.intAdicAbv_le_one

added theorem IsDedekindDomain.HeightOneSpectrum.intAdicAbv_lt_one_iff

modified theorem IsDedekindDomain.HeightOneSpectrum.isNonarchimedean_adicAbv

modified theorem IsDedekindDomain.HeightOneSpectrum.isNonarchimedean_adicAbvDef

added theorem IsDedekindDomain.HeightOneSpectrum.isNonarchimedean_intAdicAbv

added theorem IsDedekindDomain.HeightOneSpectrum.isNonarchimedean_intAdicAbvDef