Commit 2025-05-27 10:28 05f63004

View on Github →

feat(RingTheory/DedekindDomain/AdicValuation): Generalize NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv to IsDedekindDomain.HeightOneSpectrum.adicAbv (#25026) We introduce IsDedekindDomain.HeightOneSpectrum.adicAbv as a generalization of NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv for an arbitrary DedekindDomain.

Estimated changes

Modified Mathlib/NumberTheory/NumberField/FinitePlaces.lean

modified theorem NumberField.RingOfIntegers.HeightOneSpectrum.RingOfIntegers.HeightOneSpectrum.adicAbv_intCast_le_one

modified theorem NumberField.RingOfIntegers.HeightOneSpectrum.RingOfIntegers.HeightOneSpectrum.adicAbv_natCast_le_one

modified theorem NumberField.RingOfIntegers.HeightOneSpectrum.absNorm_ne_zero

added theorem NumberField.RingOfIntegers.HeightOneSpectrum.isNonarchimedean_adicAbv

modified theorem NumberField.RingOfIntegers.HeightOneSpectrum.one_lt_absNorm_nnreal

Modified Mathlib/RingTheory/DedekindDomain/AdicValuation.lean

added def IsDedekindDomain.HeightOneSpectrum.adicAbv

added def IsDedekindDomain.HeightOneSpectrum.adicAbvDef

added theorem IsDedekindDomain.HeightOneSpectrum.isNonarchimedean_adicAbv

added theorem IsDedekindDomain.HeightOneSpectrum.isNonarchimedean_adicAbvDef