Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-19 17:55 5de67573

View on Github →

chore(algebra/ordered_group): deduplicate (#5403) I deleted many a_of_b lemmas for which a_iff_b existed, then restored (most? all?) of them using alias command.

Estimated changes

deleted theorem add_le_of_le_sub_left
deleted theorem add_le_of_le_sub_right
deleted theorem add_lt_of_lt_sub_left
deleted theorem add_lt_of_lt_sub_right
deleted theorem exists_gt_zero
added theorem exists_zero_lt
deleted theorem le_add_of_neg_le_sub_left
deleted theorem le_add_of_sub_left_le
deleted theorem le_add_of_sub_right_le
deleted theorem le_of_sub_nonneg
deleted theorem le_of_sub_nonpos
deleted theorem le_sub_left_of_add_le
deleted theorem le_sub_right_of_add_le
deleted theorem lt_add_of_neg_lt_sub_left
deleted theorem lt_add_of_sub_left_lt
deleted theorem lt_add_of_sub_right_lt
deleted theorem lt_of_sub_neg
deleted theorem lt_of_sub_pos
deleted theorem lt_sub_left_of_add_lt
deleted theorem lt_sub_right_of_add_lt
deleted theorem neg_le_sub_left_of_le_add
deleted theorem neg_lt_sub_left_of_lt_add
deleted theorem sub_le_of_sub_le
deleted theorem sub_le_self
modified theorem sub_le_self_iff
deleted theorem sub_left_le_of_le_add
deleted theorem sub_left_lt_of_lt_add
deleted theorem sub_lt_of_sub_lt
deleted theorem sub_lt_self
modified theorem sub_lt_self_iff
deleted theorem sub_lt_sub_of_le_of_lt
deleted theorem sub_lt_sub_of_lt_of_le
deleted theorem sub_neg_of_lt
deleted theorem sub_nonneg_of_le
deleted theorem sub_nonpos_of_le
deleted theorem sub_pos_of_lt
deleted theorem sub_right_le_of_le_add
deleted theorem sub_right_lt_of_lt_add
deleted theorem sub_le_of_abs_sub_le_left
deleted theorem sub_lt_of_abs_sub_lt_left