Theorem IsDedekindDomain.HeightOneSpectrum.adicAbv_coe_le_one

Modification history

2026-01-03 19:24
Mathlib/RingTheory/DedekindDomain/AdicValuation.lean
feat(RingTheory/DedekindDomain/AdicValuation): introduce `intAdicAbv` (#33324) …
Modified IsDedekindDomain.HeightOneSpectrum.adicAbv_coe_le_oneView on Github →
2025-06-03 07:59
Mathlib/RingTheory/DedekindDomain/AdicValuation.lean
feat(RingTheory/DedekindDomain/AdicValuation): Generalize APIs for `adicAbv` (#25330) …
Added IsDedekindDomain.HeightOneSpectrum.adicAbv_coe_le_oneView on Github →