Theorem IsDedekindDomain.HeightOneSpectrum.valuation_div_le_one_iff

Modification history

2026-10-17 09:16
Mathlib/RingTheory/DedekindDomain/AdicValuation.lean
chore: split `RingTheory/DedekindDomain/AdicValuation.lean` into `AdicValuation/Valuation.lean` and `AdicValuation/Completion.lean` (#44666) …
Modified IsDedekindDomain.HeightOneSpectrum.valuation_div_le_one_iffView on Github →
2025-11-17 14:01
Mathlib/RingTheory/DedekindDomain/AdicValuation.lean
feat(DedekindDomain/AdicValuation): `le_one` lemmas for `HeightOneSpectrum.valuation` and specialisations to `Rat` (#30171)
Added IsDedekindDomain.HeightOneSpectrum.valuation_div_le_one_iffView on Github →