Theorem IsDedekindDomain.HeightOneSpectrum.exists_valuation_sub_lt_of_integer

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.exists_valuation_sub_lt_of_integerView on Github →
2026-05-25 14:55
Mathlib/RingTheory/DedekindDomain/AdicValuation.lean
feat: elements of Dedekind domain approximate elements of valuation ring (#37523) …
Added IsDedekindDomain.HeightOneSpectrum.exists_valuation_sub_lt_of_integerView on Github →