Theorem IsDedekindDomain.HeightOneSpectrum.intValuation_toFun

Modification history

2025-12-17 19:48

Mathlib/RingTheory/DedekindDomain/AdicValuation.lean

chore: remove March and April 2025 deprecated declarations (#32990) …

Deleted IsDedekindDomain.HeightOneSpectrum.intValuation_toFun View on Github →

2025-05-17 21:17

Mathlib/RingTheory/DedekindDomain/AdicValuation.lean

chore(RingTheory/DedekindDomain/AdicValuation): Use intValuation over intValuationDef (#24644) …

Added IsDedekindDomain.HeightOneSpectrum.intValuation_toFun View on Github →