Theorem IsDedekindDomain.HeightOneSpectrum.valuation_eq_intValuationDef

Modification history

2025-12-29 03:44
Mathlib/RingTheory/DedekindDomain/AdicValuation.lean
chore: remove May 2025 deprecated declarations (#33014) …
Deleted IsDedekindDomain.HeightOneSpectrum.valuation_eq_intValuationDefView on Github →
2025-02-21 11:42
Mathlib/RingTheory/DedekindDomain/AdicValuation.lean
chore: make arg in HeightOneSpectrum.valuation explicit (#22139) …
Modified IsDedekindDomain.HeightOneSpectrum.valuation_eq_intValuationDefView on Github →
2024-07-28 16:59
Mathlib/RingTheory/DedekindDomain/AdicValuation.lean
feat: topology on ring of finite adeles. (#14176) …
Added IsDedekindDomain.HeightOneSpectrum.valuation_eq_intValuationDefView on Github →