Theorem IsDedekindDomain.HeightOneSpectrum.intValuation_if_neg

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