Theorem NumberField.RingOfIntegers.HeightOneSpectrum.isNonarchimedean_adicAbv
Modification history
2025-05-27 10:28
Mathlib/NumberTheory/NumberField/FinitePlaces.lean
feat(RingTheory/DedekindDomain/AdicValuation): Generalize `NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv` to `IsDedekindDomain.HeightOneSpectrum.adicAbv` (#25026) …
Added NumberField.RingOfIntegers.HeightOneSpectrum.isNonarchimedean_adicAbvView on Github →