Def mabs

Modification history

2025-01-25 00:59

Mathlib/Algebra/Order/Group/Unbundled/Abs.lean

chore: ensure `inherit_doc`-ed notation is mentioned in the underlying doc-string (#20684) …

Modified mabs View on Github →

2024-07-24 08:31

Mathlib/Algebra/Order/Group/Abs.lean

chore (Algebra.Order.Group.Abs): split file into unbundled and bundled material (#15065) …

Modified mabs View on Github →

2024-01-13 13:48

Mathlib/Algebra/Order/Group/Abs.lean

refactor: Multiplicativise `abs` (#9553) …

Added mabs View on Github →