Theorem IsDedekindDomain.HeightOneSpectrum.intValuation_lt_one_iff_mem

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