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.

Estimated changes

added def WithAbs.algEquiv
modified theorem WithAbs.equiv_neg
modified theorem WithAbs.equiv_sub
modified theorem WithAbs.equiv_symm_add
modified theorem WithAbs.equiv_symm_mul
modified theorem WithAbs.equiv_symm_neg
modified theorem WithAbs.equiv_symm_sub
added theorem WithAbs.norm_eq_abv
modified def WithAbs