Theorem IsDedekindDomain.HeightOneSpectrum.intValuation_zero_lt

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