Commit 2025-05-17 21:17 ae4dda55

View on Github →

chore(RingTheory/DedekindDomain/AdicValuation): Use intValuation over intValuationDef (#24644) intValuationDef exists so that we can prove its basic properties before defining intValuation, but it shouldn't be used afterwards. Change theorems which use intValuation in their names to actually use intValution and update usages.

Estimated changes

Modified Mathlib/NumberTheory/NumberField/FinitePlaces.lean

Modified Mathlib/RingTheory/DedekindDomain/AdicValuation.lean

added theorem IsDedekindDomain.HeightOneSpectrum.intValuation_def

added theorem IsDedekindDomain.HeightOneSpectrum.intValuation_if_neg

modified theorem IsDedekindDomain.HeightOneSpectrum.intValuation_le_one

added theorem IsDedekindDomain.HeightOneSpectrum.intValuation_le_pow_iff_mem

added theorem IsDedekindDomain.HeightOneSpectrum.intValuation_lt_one_iff_mem

modified theorem IsDedekindDomain.HeightOneSpectrum.intValuation_ne_zero'

modified theorem IsDedekindDomain.HeightOneSpectrum.intValuation_ne_zero

added theorem IsDedekindDomain.HeightOneSpectrum.intValuation_toFun

deleted theorem IsDedekindDomain.HeightOneSpectrum.intValuation_zero_le

added theorem IsDedekindDomain.HeightOneSpectrum.intValuation_zero_lt

added theorem IsDedekindDomain.HeightOneSpectrum.valuation_lt_one_iff_mem

Modified Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean

Modified Mathlib/RingTheory/LaurentSeries.lean

modified theorem PowerSeries.intValuation_X