Theorem IsDedekindDomain.HeightOneSpectrum.uniformContinuous_algebraMap_liesOver

Modification history

2026-10-17 09:16
Mathlib/NumberTheory/RamificationInertia/Valuation.lean
chore: split `RingTheory/DedekindDomain/AdicValuation.lean` into `AdicValuation/Valuation.lean` and `AdicValuation/Completion.lean` (#44666) …
Modified IsDedekindDomain.HeightOneSpectrum.uniformContinuous_algebraMap_liesOverView on Github →
2026-05-28 09:20
Mathlib/NumberTheory/RamificationInertia/Valuation.lean
feat: `algebraMap K L` is uniform continuous with respect to adic topologies, when the ideal `w` of `L` lies above `v` (#34045) …
Added IsDedekindDomain.HeightOneSpectrum.uniformContinuous_algebraMap_liesOverView on Github →