Theorem IsDedekindDomain.HeightOneSpectrum.mem_integers_of_valuation_le_one

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.mem_integers_of_valuation_le_oneView on Github →
2025-01-08 18:19
Mathlib/RingTheory/DedekindDomain/AdicValuation.lean
feat(Ringtheory/DedekindDomain/AdicValuation); add mem_integers_of_valuation_le_one (#20523) …
Added IsDedekindDomain.HeightOneSpectrum.mem_integers_of_valuation_le_oneView on Github →