Def Abs.abs.unexpander

Modification history

2024-01-13 13:48
Mathlib/Algebra/Abs.lean
refactor: Multiplicativise `abs` (#9553) …
Deleted Abs.abs.unexpanderView on Github →
2023-06-29 10:29
Mathlib/Algebra/Abs.lean
feat: unexpander for `abs` notation (#5559) …
Added Abs.abs.unexpanderView on Github →