Def Valuation.IsEquiv.uniformEquiv

Modification history

2026-03-06 13:45
Mathlib/Topology/Algebra/Valued/WithVal.lean
chore(RingTheory/Valuation/RankOne): modify the definition of Valuation.RankOne using its range rather than its codomain (#26872) …
Modified Valuation.IsEquiv.uniformEquivView on Github →
2025-12-05 20:44
Mathlib/Topology/Algebra/Valued/WithVal.lean
feat: `WithVal v` and `WithVal w` are isomorphic as uniform spaces when `v` and `w` are equivalent valuations (#30133)
Added Valuation.IsEquiv.uniformEquivView on Github →