Mathlib Changelog
v4
Changelog
About
Github
Theorem
abs_sub_nonpos
Modification history
2025-03-15 13:13
Mathlib/Algebra/Order/Group/Abs.lean
chore(Order/Group/Abs): use `@[to_additive]` (#22468)
Deleted
abs_sub_nonpos
View on Github →
2024-02-23 19:51
Mathlib/Algebra/Order/Group/Abs.lean
feat: Small lemmas around |a - b| and Int.natAbs (a - b) (#10027) …
Added
abs_sub_nonpos
View on Github →