Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-01 13:24 d6bf2dd0

View on Github →

refactor(*): replace abs with vertical bar notation (#8891) The notion of an "absolute value" occurs both in algebra (e.g. lattice ordered groups) and analysis (e.g. GM and GL-spaces). I introduced a has_abs notation class in #9172, along with the conventional mathematical vertical bar notation |.| for abs. The notation vertical bar notation was already in use in some files as a local notation. This PR replaces abs with the vertical bar notation throughout mathlib.

Estimated changes

modified theorem abs_eq_one_of_pow_eq_one
modified theorem abs_sub_round
modified theorem abs_pow
modified theorem abs_le_abs_of_sq_le_sq
modified theorem abs_le_of_sq_le_sq
modified theorem abs_lt_abs_of_sq_lt_sq
modified theorem abs_lt_of_sq_lt_sq
modified theorem abs_neg_one_pow
modified theorem abs_sq
modified theorem pow_abs
modified theorem sq_abs
modified theorem sq_le_sq
modified theorem sq_lt_sq
modified theorem abs_div
modified theorem abs_inv
modified theorem abs_one_div
modified theorem abs_abs
modified theorem abs_abs_sub_abs_le_abs_sub
modified theorem abs_add
modified theorem abs_add_three
modified theorem abs_by_cases
modified theorem abs_choice
modified theorem abs_eq
modified theorem abs_eq_abs
modified theorem abs_eq_zero
modified theorem abs_le'
modified theorem abs_le
modified theorem abs_le_abs
modified theorem abs_le_max_abs_abs
modified theorem abs_lt
modified theorem abs_max_sub_max_le_abs
modified theorem abs_neg
modified theorem abs_nonneg
modified theorem abs_nonpos_iff
modified theorem abs_of_neg
modified theorem abs_of_nonneg
modified theorem abs_of_nonpos
modified theorem abs_of_pos
modified theorem abs_pos
modified theorem abs_pos_of_neg
modified theorem abs_pos_of_pos
modified theorem abs_sub_abs_le_abs_sub
modified theorem abs_sub_comm
modified theorem abs_sub_le
modified theorem abs_sub_le_iff
modified theorem abs_sub_lt_iff
modified theorem abs_zero
modified theorem eq_of_abs_sub_eq_zero
modified theorem eq_of_abs_sub_nonpos
modified theorem eq_or_eq_neg_of_abs_eq
modified theorem le_abs
modified theorem le_abs_self
modified theorem le_of_abs_le
modified theorem lt_abs
modified theorem lt_of_abs_lt
modified theorem max_sub_min_eq_abs'
modified theorem max_sub_min_eq_abs
modified theorem neg_abs_le_self
modified theorem neg_le_abs_self
modified theorem neg_le_of_abs_le
modified theorem neg_lt_of_abs_lt
modified theorem sub_le_of_abs_sub_le_left
modified theorem sub_le_of_abs_sub_le_right
modified theorem sub_lt_of_abs_sub_lt_left
modified theorem sub_lt_of_abs_sub_lt_right
modified theorem abs_cases
modified theorem abs_dvd
modified theorem abs_dvd_abs
modified theorem abs_dvd_self
modified theorem abs_eq_iff_mul_self_eq
modified theorem abs_eq_neg_self
modified theorem abs_eq_self
modified theorem abs_le_iff_mul_self_le
modified theorem abs_lt_iff_mul_self_lt
modified theorem abs_mul
modified theorem abs_mul_abs_self
modified theorem abs_mul_self
modified theorem abs_one
modified theorem abs_sub_sq
modified theorem abs_two
modified theorem dvd_abs
modified theorem even_abs
modified theorem self_dvd_abs
modified theorem complex.norm_int
modified theorem abs_norm_eq_norm
modified theorem abs_norm_sub_norm_le
modified theorem int.norm_eq_abs
modified theorem real.norm_eq_abs
modified theorem real.exp_log_eq_abs
modified theorem real.log_abs
modified theorem real.log_of_ne_zero
modified theorem real.abs_rpow_le_abs_rpow
modified theorem real.abs_rpow_of_nonneg
modified theorem is_o_pow_pow_of_abs_lt_left
modified theorem tsum_geometric_of_abs_lt_1
modified theorem complex.abs_abs
modified theorem complex.abs_im_le_abs
modified theorem complex.abs_of_real
modified theorem complex.abs_re_le_abs
modified theorem complex.int_cast_abs
modified theorem is_cau_geo_series_const
modified theorem is_cau_of_mono_bounded
modified theorem is_cau_series_of_abv_cau
modified theorem real.abs_cos_le_one
modified theorem real.abs_exp
modified theorem real.abs_sin_le_one
modified theorem real.cos_bound
modified theorem real.cos_pos_of_le_one
modified theorem real.exp_bound
modified theorem real.sin_bound
modified theorem int.abs_div_le_abs
modified theorem int.abs_eq_nat_abs
modified theorem int.coe_nat_abs
modified theorem int.div_eq_zero_of_lt_abs
modified theorem int.eq_zero_iff_abs_lt_one
modified theorem int.mod_abs
modified theorem int.mod_lt
modified theorem int.nat_abs_abs
modified theorem int.sign_mul_abs
modified theorem int.cast_nat_abs
modified theorem rat.abs_def
modified theorem rat.sqrt_eq
modified theorem real.is_cau_seq_iff_lift
modified theorem hyperreal.coe_abs
modified theorem nnreal.abs_eq
modified theorem real.coe_nnabs
modified theorem real.coe_to_nnreal_le
modified theorem real.abs_le_sqrt
modified theorem real.sqrt_mul_self_eq_abs
modified theorem real.sqrt_sq_eq_abs
modified theorem real.volume_interval
modified def liouville
modified theorem filter.germ.abs_def
modified theorem max_eq_half_add_add_abs_sub
modified theorem min_eq_half_add_sub_abs_sub
modified theorem int.dist_eq
modified theorem rat.dist_eq
modified theorem real.uniform_continuous_inv
modified theorem abs_dist
modified theorem abs_dist_sub_le
modified theorem nnreal.dist_eq
modified theorem real.dist_0_eq_abs
modified theorem real.dist_eq