Commit 2025-01-14 12:21 cbbe71d5

View on Github →

chore(Analysis/Normed/Ring/WithAbs): make equiv a ring equiv (#20713) Making WithAbs.equiv a ring equivalence (like WithAbs.ringEquiv) should make a lot of the API lemmas obsolete.

Estimated changes

modified def WithAbs.equiv
modified theorem WithAbs.equiv_add
modified theorem WithAbs.equiv_mul
modified theorem WithAbs.equiv_neg
modified theorem WithAbs.equiv_sub
modified theorem WithAbs.equiv_symm_neg
modified theorem WithAbs.equiv_symm_sub
modified theorem WithAbs.equiv_symm_zero
modified theorem WithAbs.equiv_zero