Commit 2025-09-25 12:50 d2860875

View on Github →

feat(Normed/Ring/WithAbs): apply results relating algebraMaps on WithAbs (#29944)

Estimated changes

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

added theorem WithAbs.algebraMap_left_apply

added theorem WithAbs.algebraMap_right_apply

added theorem WithAbs.equiv_algebraMap_apply