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.
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.