Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-03-14 13:51 af8f9bc2

View on Github →

chore(analysis/inner_product_space/basic): make arguments explicit (#18579) This applies the regex

\{(x[^}]+)\}(?![^\n]*↔)(?=[^\n]* =)

and replaces it with ($1) in appropriate places. The heuristic is "equalities should take their arguments explicitly". Underscores are then inserted as necessary to fix the build.

Estimated changes

modified theorem innerSL_flip_apply
modified theorem inner_abs_conj_sym
modified theorem inner_add_add_self
modified theorem inner_add_left
modified theorem inner_add_right
modified theorem inner_im_symm
modified theorem inner_mul_conj_re_abs
modified theorem inner_neg_left
modified theorem inner_neg_neg
modified theorem inner_neg_right
modified theorem inner_re_symm
modified theorem inner_re_zero_left
modified theorem inner_re_zero_right
modified theorem inner_self_abs_to_K
modified theorem inner_self_conj
modified theorem inner_self_im_zero
modified theorem inner_self_nonneg_im
modified theorem inner_self_re_abs
modified theorem inner_self_re_to_K
modified theorem inner_smul_left
modified theorem inner_smul_real_left
modified theorem inner_smul_real_right
modified theorem inner_smul_right
modified theorem inner_sub_left
modified theorem inner_sub_right
modified theorem inner_sub_sub_self
modified theorem inner_zero_left
modified theorem inner_zero_right
modified theorem norm_add_mul_self
modified theorem norm_add_mul_self_real
modified theorem norm_add_sq
modified theorem norm_add_sq_real
modified theorem norm_sub_mul_self
modified theorem norm_sub_mul_self_real
modified theorem norm_sub_sq
modified theorem norm_sub_sq_real
modified theorem real_inner_add_add_self
modified theorem real_inner_self_abs
modified theorem real_inner_smul_left
modified theorem real_inner_smul_right
modified theorem real_inner_sub_sub_self