Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-03-15 13:13
e390e207
View on Github →
chore(Order/Group/Abs): use
@[to_additive]
(
#22468
)
Estimated changes
Modified
Mathlib/Algebra/Order/Group/Abs.lean
deleted
theorem
abs_abs_sub_abs_le_abs_sub
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_le_of_nonneg_of_le
deleted
theorem
abs_sub_lt_iff
deleted
theorem
abs_sub_lt_of_nonneg_of_lt
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
added
theorem
div_le_of_mabs_div_le_left
added
theorem
div_le_of_mabs_div_le_right
added
theorem
div_lt_of_mabs_div_lt_left
added
theorem
div_lt_of_mabs_div_lt_right
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_of_le_of_le
added
theorem
mabs_div_le_of_one_le_of_le
added
theorem
mabs_div_le_one
added
theorem
mabs_div_lt_iff
added
theorem
mabs_div_lt_of_one_le_of_lt
added
theorem
mabs_div_mabs_le_mabs_div
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_mabs_div_mabs_le_mabs_div
added
theorem
mabs_max_le_max_mabs_mabs
added
theorem
mabs_min_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
added
theorem
max_one_mul_max_inv_one_eq_mabs_self
deleted
theorem
max_zero_add_max_neg_zero_eq_abs_self
deleted
theorem
min_abs_abs_le_abs_max
deleted
theorem
min_abs_abs_le_abs_min
added
theorem
min_mabs_mabs_le_mabs_max
added
theorem
min_mabs_mabs_le_mabs_min
deleted
theorem
neg_le_of_abs_le
deleted
theorem
sub_le_of_abs_sub_le_left
deleted
theorem
sub_le_of_abs_sub_le_right
deleted
theorem
sub_lt_of_abs_sub_lt_left
deleted
theorem
sub_lt_of_abs_sub_lt_right