Theorem Valuation.IsEquiv.uniformContinuous_equivWithVal

Modification history

2026-03-02 10:51
Mathlib/Topology/Algebra/Valued/WithVal.lean
refactor: use 1-field structure to define the `WithVal` type synonym (#34049) …
Deleted Valuation.IsEquiv.uniformContinuous_equivWithValView 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.uniformContinuous_equivWithValView on Github →