Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-18 21:30 23cf025c

View on Github →

feat(algebra/ordered_sub): define truncated subtraction in general (#8503)

  • Define and prove properties of truncated subtraction in general
  • We currently only instantiate it for nat. The other types (multiset, finsupp, nnreal, ennreal, ...) will be in future PRs. Todo in future PRs:
  • Provide has_ordered_sub instances for all specific cases
  • Remove the lemmas specific to each individual type

Estimated changes

added theorem lt_iff_exists_mul
modified theorem min_mul_distrib'
modified theorem min_mul_distrib
added theorem min_one
added theorem one_min
added theorem mul_left_cancel''
added theorem mul_right_cancel''
added theorem add_le_add_add_sub
added theorem add_sub_assoc_of_le
added theorem add_sub_cancel_iff_le
added theorem add_sub_cancel_left
added theorem add_sub_cancel_of_le
added theorem add_sub_cancel_right
added theorem add_sub_eq_max
added theorem add_sub_le_assoc
added theorem add_sub_le_left
added theorem add_sub_le_right
added theorem add_sub_sub_cancel'
added theorem eq_sub_of_add_eq''
added theorem le_add_sub'
added theorem le_add_sub
added theorem le_add_sub_swap
added theorem le_sub_add
added theorem le_sub_add_add
added theorem le_sub_iff_le_sub
added theorem le_sub_iff_left
added theorem le_sub_iff_right
added theorem le_sub_of_add_le_left'
added theorem lt_add_of_sub_lt_left'
added theorem lt_of_sub_lt_sub_left
added theorem lt_of_sub_lt_sub_right
added theorem lt_sub_iff_left
added theorem lt_sub_iff_left_of_le
added theorem lt_sub_iff_lt_sub
added theorem lt_sub_iff_right
added theorem lt_sub_iff_right_of_le
added theorem lt_sub_of_add_lt_left
added theorem lt_sub_of_add_lt_right
added theorem sub_add_cancel_iff_le
added theorem sub_add_cancel_of_le
added theorem sub_add_eq_add_sub'
added theorem sub_add_eq_max
added theorem sub_add_eq_sub_sub'
added theorem sub_add_min
added theorem sub_add_sub_cancel''
added theorem sub_eq_of_eq_add''
added theorem sub_eq_sub_min
added theorem sub_eq_zero_iff_le
added theorem sub_inj_left
added theorem sub_inj_right
added theorem sub_le_iff_left
added theorem sub_le_iff_right
added theorem sub_le_iff_sub_le
added theorem sub_le_self'
added theorem sub_le_sub'
added theorem sub_le_sub_add_sub
added theorem sub_le_sub_iff_left'
added theorem sub_le_sub_iff_right'
added theorem sub_le_sub_left'
added theorem sub_le_sub_right'
added theorem sub_left_inj'
added theorem sub_lt_iff_left
added theorem sub_lt_iff_right
added theorem sub_lt_iff_sub_lt
added theorem sub_lt_self'
added theorem sub_lt_self_iff'
added theorem sub_lt_sub_iff_right'
added theorem sub_lt_sub_right_of_le
added theorem sub_min
added theorem sub_pos_iff_lt
added theorem sub_pos_iff_not_le
added theorem sub_pos_of_lt'
added theorem sub_right_comm'
added theorem sub_right_inj'
added theorem sub_self'
added theorem sub_self_add
added theorem sub_sub'
added theorem sub_sub_assoc
added theorem sub_sub_cancel_of_le
added theorem sub_sub_le
added theorem sub_sub_sub_le_sub
added theorem sub_zero'
added theorem zero_sub'
deleted theorem nat.add_sub_cancel_right
deleted theorem nat.add_sub_eq_max
deleted theorem nat.sub_add_eq_max
deleted theorem nat.sub_add_min
deleted theorem nat.sub_min