Def WithAbs.algEquiv

Modification history

2025-02-10 20:34

Mathlib/Analysis/Normed/Ring/WithAbs.lean

feat/chore(Analysis/Normed/Ring/WithAbs): extend API for WithAbs (#20642) …

Added WithAbs.algEquiv View on Github →