Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-20 15:39 68a674ef

View on Github →

refactor(algebra/order/sub): rename sub -> tsub (#9793)

  • Renames lemmas in the file algebra/order/sub to use tsub instead of sub in the name
  • Remove primes from lemma names where possible
  • Zulip thread
  • Remove sub_mul_ge, mul_sub_ge and lt_sub_iff_lt_sub. They were special cases of le_sub_mul, le_mul_sub and lt_sub_comm, respectively.

Estimated changes

deleted theorem mul_sub_ge
deleted theorem sub_mul_ge
deleted theorem add_hom.le_map_sub
added theorem add_hom.le_map_tsub
deleted theorem add_le_add_add_sub
added theorem add_le_add_add_tsub
deleted theorem add_monoid_hom.le_map_sub
deleted theorem add_sub_add_eq_sub_left'
deleted theorem add_sub_add_right_eq_sub'
deleted theorem add_sub_assoc_of_le
deleted theorem add_sub_cancel_iff_le
deleted theorem add_sub_cancel_left
deleted theorem add_sub_cancel_of_le
deleted theorem add_sub_cancel_right
deleted theorem add_sub_eq_max
deleted theorem add_sub_le_assoc
deleted theorem add_sub_le_left
deleted theorem add_sub_le_right
deleted theorem add_sub_sub_cancel'
added theorem add_tsub_assoc_of_le
added theorem add_tsub_cancel_iff_le
added theorem add_tsub_cancel_left
added theorem add_tsub_cancel_of_le
added theorem add_tsub_cancel_right
added theorem add_tsub_eq_max
added theorem add_tsub_le_assoc
added theorem add_tsub_le_left
added theorem add_tsub_le_right
added theorem add_tsub_tsub_cancel
deleted theorem eq_sub_iff_add_eq_of_le
deleted theorem eq_sub_of_add_eq''
added theorem eq_tsub_of_add_eq
deleted theorem le_add_sub'
deleted theorem le_add_sub
deleted theorem le_add_sub_swap
added theorem le_add_tsub'
added theorem le_add_tsub
added theorem le_add_tsub_swap
deleted theorem le_mul_sub
added theorem le_mul_tsub
deleted theorem le_sub_add
deleted theorem le_sub_add_add
deleted theorem le_sub_iff_le_sub
deleted theorem le_sub_iff_left
deleted theorem le_sub_iff_right
deleted theorem le_sub_mul
deleted theorem le_sub_of_add_le_left'
deleted theorem le_sub_of_add_le_right'
added theorem le_tsub_add
added theorem le_tsub_add_add
added theorem le_tsub_iff_le_tsub
added theorem le_tsub_iff_left
added theorem le_tsub_iff_right
added theorem le_tsub_mul
added theorem le_tsub_of_add_le_left
deleted theorem lt_add_of_sub_lt_left'
deleted theorem lt_add_of_sub_lt_right'
added theorem lt_add_of_tsub_lt_left
deleted theorem lt_of_sub_lt_sub_left
deleted theorem lt_of_sub_lt_sub_right
deleted theorem lt_sub_comm
deleted theorem lt_sub_iff_left
deleted theorem lt_sub_iff_left_of_le
deleted theorem lt_sub_iff_lt_sub
deleted theorem lt_sub_iff_right
deleted theorem lt_sub_iff_right_of_le
deleted theorem lt_sub_of_add_lt_left
deleted theorem lt_sub_of_add_lt_right
added theorem lt_tsub_comm
added theorem lt_tsub_iff_left
added theorem lt_tsub_iff_left_of_le
added theorem lt_tsub_iff_right
added theorem lt_tsub_of_add_lt_left
deleted theorem order_iso.map_sub
added theorem order_iso.map_tsub
deleted theorem sub_add_cancel_iff_le
deleted theorem sub_add_cancel_of_le
deleted theorem sub_add_eq_add_sub'
deleted theorem sub_add_eq_max
deleted theorem sub_add_eq_sub_sub'
deleted theorem sub_add_eq_sub_sub_swap'
deleted theorem sub_add_min
deleted theorem sub_add_sub_cancel''
deleted theorem sub_eq_iff_eq_add_of_le
deleted theorem sub_eq_of_eq_add''
deleted theorem sub_eq_of_eq_add_rev
deleted theorem sub_eq_sub_min
deleted theorem sub_eq_zero_iff_le
deleted theorem sub_inj_left
deleted theorem sub_inj_right
deleted theorem sub_le_iff_left
deleted theorem sub_le_iff_right
deleted theorem sub_le_iff_sub_le
deleted theorem sub_le_self'
deleted theorem sub_le_sub'
deleted theorem sub_le_sub_add_sub
deleted theorem sub_le_sub_iff_left'
deleted theorem sub_le_sub_iff_right'
deleted theorem sub_le_sub_left'
deleted theorem sub_le_sub_right'
deleted theorem sub_left_inj'
deleted theorem sub_lt_iff_left
deleted theorem sub_lt_iff_right
deleted theorem sub_lt_iff_sub_lt
deleted theorem sub_lt_self'
deleted theorem sub_lt_self_iff'
deleted theorem sub_lt_sub_iff_left_of_le
deleted theorem sub_lt_sub_iff_right'
deleted theorem sub_lt_sub_right_of_le
deleted theorem sub_min
deleted theorem sub_pos_iff_lt
deleted theorem sub_pos_iff_not_le
deleted theorem sub_pos_of_lt'
deleted theorem sub_right_comm'
deleted theorem sub_right_inj'
deleted theorem sub_self'
deleted theorem sub_self_add
deleted theorem sub_sub'
deleted theorem sub_sub_assoc
deleted theorem sub_sub_cancel_of_le
deleted theorem sub_sub_le
deleted theorem sub_sub_sub_cancel_right'
deleted theorem sub_sub_sub_le_sub
deleted theorem sub_zero'
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_eq_tsub_tsub
added theorem tsub_add_min
added theorem tsub_add_tsub_cancel
added theorem tsub_eq_of_eq_add
added theorem tsub_eq_of_eq_add_rev
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_iff_left
added theorem tsub_le_iff_right
added theorem tsub_le_iff_tsub_le
added theorem tsub_le_self
added theorem tsub_le_tsub
added theorem tsub_le_tsub_add_tsub
added theorem tsub_le_tsub_iff_left
added theorem tsub_le_tsub_iff_right
added theorem tsub_le_tsub_left
added theorem tsub_le_tsub_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_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_comm
added theorem tsub_right_inj
added theorem tsub_self
added theorem tsub_self_add
added theorem tsub_tsub
added theorem tsub_tsub_assoc
added theorem tsub_tsub_cancel_of_le
added theorem tsub_tsub_le
added theorem tsub_tsub_tsub_le_tsub
added theorem tsub_zero
deleted theorem zero_sub'
added theorem zero_tsub
modified theorem multiset.eq_union_left
modified theorem multiset.le_union_left
modified theorem ennreal.lt_sub_comm
modified theorem ennreal.lt_sub_iff_add_lt