Theorem abs_eq_self

Modification history

2023-10-30 03:57

Mathlib/Algebra/Order/Group/Abs.lean

refactor: generalize Abs lemmas from rings to groups (#7976) …

Modified abs_eq_self View on Github →

2022-12-10 13:41

Mathlib/Algebra/Order/Ring/Abs.lean

feat port: Algebra.Order.Ring.Abs (#929) …

Added abs_eq_self View on Github →