Commit 2022-12-01 16:13 147bb19c

View on Github →

feat: port Algebra.Order.Sub.Canonical (#814) mathlib3 SHA: 62a5626868683c104774de8d85b9855234ac807c Note that the simpNF linter thinks that some of the lemmas are incorrectly written. I'm not sure what the intended fix is.

Estimated changes

added theorem add_tsub_assoc_of_le
added theorem add_tsub_cancel_iff_le
added theorem add_tsub_cancel_of_le
added theorem add_tsub_eq_max
added theorem add_tsub_tsub_cancel
added theorem le_tsub_iff_le_tsub
added theorem le_tsub_iff_left
added theorem le_tsub_iff_right
added theorem lt_tsub_iff_left_of_le
added theorem tsub_add_cancel_iff_le
added theorem tsub_add_cancel_of_le
added theorem tsub_add_eq_add_tsub
added theorem tsub_add_eq_max
added theorem tsub_add_min
added theorem tsub_add_tsub_cancel
added theorem tsub_add_tsub_comm
added theorem tsub_eq_tsub_min
added theorem tsub_eq_zero_iff_le
added theorem tsub_inj_left
added theorem tsub_inj_right
added theorem tsub_le_self
added theorem tsub_le_tsub_iff_left
added theorem tsub_le_tsub_iff_right
added theorem tsub_left_inj
added theorem tsub_lt_iff_left
added theorem tsub_lt_iff_right
added theorem tsub_lt_iff_tsub_lt
added theorem tsub_lt_of_lt
added theorem tsub_lt_self
added theorem tsub_lt_self_iff
added theorem tsub_lt_tsub_iff_right
added theorem tsub_min
added theorem tsub_pos_iff_lt
added theorem tsub_pos_iff_not_le
added theorem tsub_pos_of_lt
added theorem tsub_right_inj
added theorem tsub_self
added theorem tsub_self_add
added theorem tsub_tsub_assoc
added theorem tsub_tsub_cancel_of_le
added theorem zero_tsub