Theorem IsDedekindDomain.HeightOneSpectrum.isNonarchimedean_adicAbvDef

Modification history

2026-01-03 19:24
Mathlib/RingTheory/DedekindDomain/AdicValuation.lean
feat(RingTheory/DedekindDomain/AdicValuation): introduce `intAdicAbv` (#33324) …
Modified IsDedekindDomain.HeightOneSpectrum.isNonarchimedean_adicAbvDefView on Github →
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_adicAbvDefView on Github →