Commit 2025-06-03 07:59 bedb4966

View on Github →

feat(RingTheory/DedekindDomain/AdicValuation): Generalize APIs for adicAbv (#25330) We generalize three theorems about NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv to IsDedekindDomain.HeightOneSpectrum.adicAbv.

Estimated changes

Modified Mathlib/NumberTheory/NumberField/FinitePlaces.lean

Modified Mathlib/RingTheory/DedekindDomain/AdicValuation.lean

added theorem IsDedekindDomain.HeightOneSpectrum.adicAbv_coe_eq_one_iff

added theorem IsDedekindDomain.HeightOneSpectrum.adicAbv_coe_le_one

added theorem IsDedekindDomain.HeightOneSpectrum.adicAbv_coe_lt_one_iff