Theorem IsDedekindDomain.HeightOneSpectrum.valuation_exists_uniformizer'

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

2026-04-16 12:42

Mathlib/RingTheory/DedekindDomain/AdicValuation.lean

feat: localizations of primes in Dedekind domains are valuation subrings (#33010) …

Added IsDedekindDomain.HeightOneSpectrum.valuation_exists_uniformizer'View on Github →