Commit 2022-11-27 22:58 3df696e4

View on Github →

feat: port Algebra.Order.Sub.Defs (#732) Based on '71ca477041bcd6d7c745fe555dc49735c12944b7'

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Order/Sub/Defs.lean

added theorem add_le_add_add_tsub

added theorem add_tsub_add_eq_tsub_left

added theorem add_tsub_add_eq_tsub_right

added theorem add_tsub_add_le_tsub_add_tsub

added theorem add_tsub_add_le_tsub_left

added theorem add_tsub_add_le_tsub_right

added theorem add_tsub_cancel_left

added theorem add_tsub_cancel_right

added theorem add_tsub_le_assoc

added theorem add_tsub_le_left

added theorem add_tsub_le_right

added theorem add_tsub_le_tsub_add

added theorem antitone_const_tsub

added theorem eq_tsub_of_add_eq

added theorem le_add_tsub'

added theorem le_add_tsub

added theorem le_add_tsub_swap

added theorem le_tsub_add

added theorem le_tsub_add_add

added theorem le_tsub_of_add_le_left

added theorem le_tsub_of_add_le_right

added theorem lt_add_of_tsub_lt_left

added theorem lt_add_of_tsub_lt_right

added theorem lt_of_tsub_lt_tsub_left

added theorem lt_of_tsub_lt_tsub_right

added theorem lt_tsub_comm

added theorem lt_tsub_iff_left

added theorem lt_tsub_iff_right

added theorem lt_tsub_of_add_lt_left

added theorem lt_tsub_of_add_lt_right

added theorem tsub_add_eq_tsub_tsub

added theorem tsub_add_eq_tsub_tsub_swap

added theorem tsub_eq_of_eq_add

added theorem tsub_eq_of_eq_add_rev

added theorem tsub_le_iff_left

added theorem tsub_le_iff_right

added theorem tsub_le_iff_tsub_le

added theorem tsub_le_tsub

added theorem tsub_le_tsub_add_tsub

added theorem tsub_le_tsub_left

added theorem tsub_le_tsub_right

added theorem tsub_nonpos

added theorem tsub_right_comm

added theorem tsub_tsub

added theorem tsub_tsub_le

added theorem tsub_tsub_le_tsub_add

added theorem tsub_tsub_tsub_le_tsub

added theorem tsub_zero