2025-10-01 15:29
Mathlib/Analysis/AbsoluteValue/Equivalence.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 AbsoluteValue.IsEquiv.isEmbedding_equivWithAbs