Theorem IsDedekindDomain.HeightOneSpectrum.isNonarchimedean_adicAbvDef

Modification history

2025-05-27 10:28

Mathlib/RingTheory/DedekindDomain/AdicValuation.lean

feat(RingTheory/DedekindDomain/AdicValuation): Generalize `NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv` to `IsDedekindDomain.HeightOneSpectrum.adicAbv` (#25026) …

Added IsDedekindDomain.HeightOneSpectrum.isNonarchimedean_adicAbvDef View on Github →