Mathlib Changelog
v4
Changelog
About
Github
Theorem
IsDedekindDomain.HeightOneSpectrum.intValuation_def
Modification history
2025-05-17 21:17
Mathlib/RingTheory/DedekindDomain/AdicValuation.lean
chore(RingTheory/DedekindDomain/AdicValuation): Use intValuation over intValuationDef (#24644) …
Added
IsDedekindDomain.HeightOneSpectrum.intValuation_def
View on Github →