Commit 2025-02-10 20:34 1b7148b5
View on Github →feat/chore(Analysis/Normed/Ring/WithAbs): extend API for WithAbs (#20642)
This PR extends the API around WithAbs
by adding more instances, the algebra equivalence WithAbs.algEquiv
and a rewriting lemma norm --> absolute value.