Theorem WithAbs.equivWithAbs_symm

Modification history

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.equivWithAbs_symmView on Github →