Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-12 20:50 d3d70f1f

View on Github →

chore(algebra/order*): move abs/min/max, review (#4581)

  • make algebra.ordered_group import algebra.order_functions, not vice versa;
  • move some proofs from algebra.ordered_functions to algebra.ordered_group and algebra.ordered_ring;
  • deduplicate API;
  • golf some proofs.

Estimated changes

deleted theorem abs_abs_sub_le_abs_sub
deleted theorem abs_add
deleted theorem abs_eq
deleted theorem abs_eq_zero
deleted theorem abs_le
deleted theorem abs_le_abs
deleted theorem abs_le_max_abs_abs
deleted theorem abs_lt
deleted theorem abs_max_sub_max_le_abs
deleted theorem abs_nonpos_iff
deleted theorem abs_one
deleted theorem abs_pos_iff
deleted theorem abs_sub_le_iff
deleted theorem abs_sub_lt_iff
deleted theorem fn_min_mul_fn_max
deleted theorem lt_abs
deleted theorem max_le_add_of_nonneg
deleted theorem max_mul_of_nonneg
deleted theorem max_sub_min_eq_abs'
deleted theorem max_sub_min_eq_abs
deleted theorem max_zero_sub_eq_self
deleted theorem min_le_add_of_nonneg_left
deleted theorem min_mul_max
deleted theorem min_mul_of_nonneg
deleted theorem min_sub
deleted theorem mul_max_of_nonneg
deleted theorem mul_min_of_nonneg
deleted theorem sub_abs_le_abs_sub
added theorem max_div_div_right
added theorem min_div_div_right
modified theorem abs_abs
added theorem abs_add
deleted theorem abs_add_le_abs_add_abs
added theorem abs_eq
added theorem abs_eq_zero
added theorem abs_le'
added theorem abs_le
added theorem abs_le_abs
added theorem abs_le_max_abs_abs
deleted theorem abs_le_of_le_of_neg_le
added theorem abs_lt
deleted theorem abs_lt_of_lt_of_neg_lt
added theorem abs_max_sub_max_le_abs
modified theorem abs_neg
added theorem abs_nonpos_iff
modified theorem abs_of_neg
modified theorem abs_of_nonneg
modified theorem abs_of_nonpos
modified theorem abs_of_pos
added theorem abs_pos
deleted theorem abs_pos_of_ne_zero
modified theorem abs_pos_of_neg
modified theorem abs_pos_of_pos
added theorem abs_sub_le_iff
added theorem abs_sub_lt_iff
modified theorem abs_zero
added theorem eq_of_abs_sub_nonpos
deleted theorem eq_zero_of_abs_eq_zero
added theorem fn_min_mul_fn_max
modified theorem le_abs_self
added theorem lt_abs
deleted theorem max_eq_neg_min_neg_neg
added theorem max_le_add_of_nonneg
modified theorem max_neg_neg
added theorem max_sub_min_eq_abs'
added theorem max_sub_min_eq_abs
added theorem max_sub_sub_left
added theorem max_sub_sub_right
added theorem max_zero_sub_eq_self
deleted theorem min_eq_neg_max_neg_neg
added theorem min_mul_max
modified theorem min_neg_neg
added theorem min_sub_sub_left
added theorem min_sub_sub_right
deleted theorem ne_zero_of_abs_ne_zero
modified theorem neg_le_abs_self
added def abs_hom
added theorem abs_one
added theorem max_mul_of_nonneg
added theorem min_mul_of_nonneg
added theorem mul_max_of_nonneg
added theorem mul_min_of_nonneg