2025-10-01 15:29
Mathlib/Analysis/Normed/Ring/WithAbs.lean
feat(AbsoluteValue/Equivalence): two absolute values `v` and `w` are equivalent if and only if `WithAbs v` and `WithAbs w` are homeomorphic (#29966)
Added WithAbs.equiv_equivWithAbs_symm_apply