Commit 2025-12-05 20:44 07946e86

View on Github →

feat: WithVal v and WithVal w are isomorphic as uniform spaces when v and w are equivalent valuations (#30133)

Estimated changes

Modified Mathlib/Algebra/Order/Hom/Ring.lean

added theorem OrderRingIso.apply_symm_apply

added theorem OrderRingIso.lt_symm_apply

added theorem OrderRingIso.symm_apply_apply

added theorem OrderRingIso.symm_apply_lt

Modified Mathlib/RingTheory/Valuation/Basic.lean

added theorem Valuation.IsEquiv.pos_iff

Modified Mathlib/Topology/Algebra/Valued/WithVal.lean

added def Valuation.IsEquiv.orderRingIso

added theorem Valuation.IsEquiv.orderRingIso_apply

added theorem Valuation.IsEquiv.orderRingIso_symm_apply

added theorem Valuation.IsEquiv.uniformContinuous_equivWithVal

added def Valuation.IsEquiv.uniformEquiv

added def WithVal.equivWithVal

added theorem WithVal.equivWithVal_apply

added theorem WithVal.equivWithVal_symm

added theorem WithVal.equivWithVal_symm_apply

added theorem WithVal.le_def

added theorem WithVal.lt_def