Theorem OrderRingIso.lt_symm_apply

Modification history

2025-12-05 20:44
Mathlib/Algebra/Order/Hom/Ring.lean
feat: `WithVal v` and `WithVal w` are isomorphic as uniform spaces when `v` and `w` are equivalent valuations (#30133)
Added OrderRingIso.lt_symm_applyView on Github →