mathlib3
4b1a0577 - feat(algebra/order/sub): An `add_group` has ordered subtraction (#10225)

Commit
4 years ago
feat(algebra/order/sub): An `add_group` has ordered subtraction (#10225) This wraps up `sub_le_iff_le_add` in an `has_ordered_sub` instance.
Author
Parents
Loading