Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-25 01:36 5f543bd9

View on Github →

chore(algebra/order/sub): Generalize lemmas (#15497) Generalize many lemmas from canonically_ordered_add_monoid to has_exists_add_of_le, and a few other generalizations.

New lemmas

  • mul_le_cancellable_one/add_le_cancellable_zero
  • tsub_add_le_right_comm
  • add_tsub_add_le_tsub_left
  • add_tsub_add_le_tsub_right

Estimated changes

added theorem mul_le_cancellable_one
added theorem add_tsub_le_tsub_add
modified theorem lt_tsub_of_add_lt_left
modified theorem lt_tsub_of_add_lt_right
modified theorem tsub_add_eq_tsub_tsub
modified theorem tsub_add_tsub_cancel
deleted theorem tsub_eq_zero_of_le
modified theorem tsub_inj_left
modified theorem tsub_le_self
modified theorem tsub_lt_of_lt
modified theorem tsub_pos_of_lt
modified theorem tsub_self
modified theorem tsub_self_add
modified theorem zero_tsub