Theorem WithVal.equivWithVal_symm

Modification history

2026-08-11 12:14
Mathlib/Topology/Algebra/Valued/WithVal.lean
chore: delete deprecated declarations/modules from January 2026 (#42075) …
Deleted WithVal.equivWithVal_symmView 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 WithVal.equivWithVal_symmView on Github →