Commit 2025-10-01 15:29 3cf53880

View on Github →

feat(AbsoluteValue/Equivalence): two absolute values v and w are equivalent if and only if WithAbs v and WithAbs w are homeomorphic (#29966)

Estimated changes

Modified Mathlib/Analysis/AbsoluteValue/Equivalence.lean

added theorem AbsoluteValue.IsEquiv.equivWithAbs_image_mem_nhds_zero

added theorem AbsoluteValue.IsEquiv.isEmbedding_equivWithAbs

added theorem AbsoluteValue.isEquiv_iff_isHomeomorph

Modified Mathlib/Analysis/Normed/Ring/WithAbs.lean

added def WithAbs.equivWithAbs

added theorem WithAbs.equivWithAbs_equiv_symm_apply

added theorem WithAbs.equivWithAbs_symm

added theorem WithAbs.equivWithAbs_symm_equiv_symm_apply

added theorem WithAbs.equiv_equivWithAbs_symm_apply