Def WithAbs

Modification history

2025-02-10 20:34

Mathlib/Analysis/Normed/Ring/WithAbs.lean

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

Modified WithAbs View on Github →

2024-10-22 07:59

Mathlib/Algebra/Ring/WithAbs.lean

feat: `WithAbs` type synonym (#17998) …

Added WithAbs View on Github →