Commit 2025-03-15 13:13 e390e207

View on Github →

chore(Order/Group/Abs): use @[to_additive] (#22468)

Estimated changes

deleted theorem abs_add'
deleted theorem abs_add
deleted theorem abs_add_three
deleted theorem abs_cases
deleted theorem abs_eq
deleted theorem abs_eq_neg_self
deleted theorem abs_eq_self
deleted theorem abs_le
deleted theorem abs_le_max_abs_abs
deleted theorem abs_max_le_max_abs_abs
deleted theorem abs_min_le_max_abs_abs
deleted theorem abs_sub
deleted theorem abs_sub_abs_le_abs_sub
deleted theorem abs_sub_le
deleted theorem abs_sub_le_iff
deleted theorem abs_sub_lt_iff
deleted theorem abs_sub_nonpos
deleted theorem abs_sub_pos
modified theorem apply_abs_le_mul_of_one_le'
modified theorem apply_abs_le_mul_of_one_le
deleted theorem dist_bdd_within_interval
deleted theorem eq_of_abs_sub_eq_zero
deleted theorem eq_of_abs_sub_le_all
deleted theorem eq_of_abs_sub_lt_all
deleted theorem eq_of_abs_sub_nonpos
added theorem eq_of_mabs_div_eq_one
added theorem eq_of_mabs_div_le_all
added theorem eq_of_mabs_div_le_one
added theorem eq_of_mabs_div_lt_all
added theorem inv_le_of_mabs_le
deleted theorem le_abs'
added theorem le_mabs'
deleted theorem le_of_abs_le
added theorem le_of_mabs_le
added theorem mabs_cases
added theorem mabs_div
added theorem mabs_div_le
added theorem mabs_div_le_iff
added theorem mabs_div_le_one
added theorem mabs_div_lt_iff
added theorem mabs_div_pos
added theorem mabs_eq
added theorem mabs_eq_inv_self
added theorem mabs_eq_self
added theorem mabs_le
added theorem mabs_le_max_mabs_mabs
added theorem mabs_mul'
added theorem mabs_mul
modified theorem mabs_mul_eq_mul_mabs_iff
added theorem mabs_mul_three
modified theorem mabs_pow
deleted theorem min_abs_abs_le_abs_max
deleted theorem min_abs_abs_le_abs_min
deleted theorem neg_le_of_abs_le
deleted theorem sub_le_of_abs_sub_le_left
deleted theorem sub_lt_of_abs_sub_lt_left