Theorem IsDedekindDomain.HeightOneSpectrum.intValuation_toFun

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_toFun View on Github →