Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-19 10:24 4ad74aed

View on Github →

chore(algebra/order/sub): Generalize to preorder and add_comm_semigroup (#11463) This generalizes a bunch of lemmas from partial_order to preorder and from add_comm_monoid to add_comm_semigroup. It also adds tsub_tsub_le_tsub_add : a - (b - c) ≤ a - b + c.

Estimated changes