Commit 2025-01-27 13:29 e779c77e

View on Github →

chore(Data/Complex/Exponential): split trig functions to new file (#21075) This PR splits Data/Complex/Exponential.lean into a new Trigonometric.lean file, addressing an instance of a long file linter trigger.

Estimated changes

deleted theorem Complex.abs_exp
deleted def Complex.cos
deleted theorem Complex.cos_add
deleted theorem Complex.cos_add_cos
deleted theorem Complex.cos_add_mul_I
deleted theorem Complex.cos_add_sin_I
deleted theorem Complex.cos_conj
deleted theorem Complex.cos_eq
deleted theorem Complex.cos_mul_I
deleted theorem Complex.cos_neg
deleted theorem Complex.cos_ofReal_im
deleted theorem Complex.cos_ofReal_re
deleted theorem Complex.cos_sq'
deleted theorem Complex.cos_sq
deleted theorem Complex.cos_sq_add_sin_sq
deleted theorem Complex.cos_sub
deleted theorem Complex.cos_sub_cos
deleted theorem Complex.cos_sub_sin_I
deleted theorem Complex.cos_three_mul
deleted theorem Complex.cos_two_mul'
deleted theorem Complex.cos_two_mul
deleted theorem Complex.cos_zero
deleted def Complex.cosh
deleted theorem Complex.cosh_add
deleted theorem Complex.cosh_add_sinh
deleted theorem Complex.cosh_conj
deleted theorem Complex.cosh_mul_I
deleted theorem Complex.cosh_neg
deleted theorem Complex.cosh_ofReal_im
deleted theorem Complex.cosh_ofReal_re
deleted theorem Complex.cosh_sq
deleted theorem Complex.cosh_sub
deleted theorem Complex.cosh_sub_sinh
deleted theorem Complex.cosh_three_mul
deleted theorem Complex.cosh_two_mul
deleted theorem Complex.cosh_zero
deleted def Complex.cot
deleted theorem Complex.cot_conj
deleted theorem Complex.exp_add_mul_I
deleted theorem Complex.exp_im
deleted theorem Complex.exp_mul_I
deleted theorem Complex.exp_re
deleted theorem Complex.exp_sub_cosh
deleted theorem Complex.exp_sub_sinh
deleted theorem Complex.ofReal_cos
deleted theorem Complex.ofReal_cosh
deleted theorem Complex.ofReal_cot
deleted theorem Complex.ofReal_sin
deleted theorem Complex.ofReal_sinh
deleted theorem Complex.ofReal_tan
deleted theorem Complex.ofReal_tanh
deleted def Complex.sin
deleted theorem Complex.sin_add
deleted theorem Complex.sin_add_mul_I
deleted theorem Complex.sin_add_sin
deleted theorem Complex.sin_conj
deleted theorem Complex.sin_eq
deleted theorem Complex.sin_mul_I
deleted theorem Complex.sin_neg
deleted theorem Complex.sin_ofReal_im
deleted theorem Complex.sin_ofReal_re
deleted theorem Complex.sin_sq
deleted theorem Complex.sin_sq_add_cos_sq
deleted theorem Complex.sin_sub
deleted theorem Complex.sin_sub_sin
deleted theorem Complex.sin_three_mul
deleted theorem Complex.sin_two_mul
deleted theorem Complex.sin_zero
deleted def Complex.sinh
deleted theorem Complex.sinh_add
deleted theorem Complex.sinh_add_cosh
deleted theorem Complex.sinh_conj
deleted theorem Complex.sinh_mul_I
deleted theorem Complex.sinh_neg
deleted theorem Complex.sinh_ofReal_im
deleted theorem Complex.sinh_ofReal_re
deleted theorem Complex.sinh_sq
deleted theorem Complex.sinh_sub
deleted theorem Complex.sinh_sub_cosh
deleted theorem Complex.sinh_three_mul
deleted theorem Complex.sinh_two_mul
deleted theorem Complex.sinh_zero
deleted def Complex.tan
deleted theorem Complex.tan_conj
deleted theorem Complex.tan_mul_I
deleted theorem Complex.tan_mul_cos
deleted theorem Complex.tan_neg
deleted theorem Complex.tan_ofReal_im
deleted theorem Complex.tan_ofReal_re
deleted theorem Complex.tan_zero
deleted def Complex.tanh
deleted theorem Complex.tanh_conj
deleted theorem Complex.tanh_mul_I
deleted theorem Complex.tanh_neg
deleted theorem Complex.tanh_ofReal_im
deleted theorem Complex.tanh_ofReal_re
deleted theorem Complex.tanh_zero
deleted theorem Complex.two_cos
deleted theorem Complex.two_cosh
deleted theorem Complex.two_sin
deleted theorem Complex.two_sinh
deleted theorem Real.abs_cos_le_one
deleted theorem Real.abs_sin_le_one
deleted theorem Real.cos_abs
deleted theorem Real.cos_bound
deleted theorem Real.cos_le_one
deleted theorem Real.cos_neg
deleted theorem Real.cos_one_le
deleted theorem Real.cos_one_pos
deleted theorem Real.cos_pos_of_le_one
deleted theorem Real.cos_sq'
deleted theorem Real.cos_sq_add_sin_sq
deleted theorem Real.cos_sq_le_one
deleted theorem Real.cos_sub
deleted theorem Real.cos_two_neg
deleted theorem Real.cos_zero
deleted theorem Real.cosh_abs
deleted theorem Real.cosh_add_sinh
deleted theorem Real.cosh_eq
deleted theorem Real.cosh_neg
deleted theorem Real.cosh_pos
deleted theorem Real.cosh_sq'
deleted theorem Real.cosh_sq_sub_sinh_sq
deleted theorem Real.cosh_sub
deleted theorem Real.cosh_sub_sinh
deleted theorem Real.cosh_zero
deleted theorem Real.exp_sub_cosh
deleted theorem Real.exp_sub_sinh
deleted theorem Real.inv_one_add_tan_sq
deleted theorem Real.neg_one_le_cos
deleted theorem Real.neg_one_le_sin
deleted theorem Real.sin_bound
deleted theorem Real.sin_le_one
deleted theorem Real.sin_neg
deleted theorem Real.sin_sq
deleted theorem Real.sin_sq_eq_half_sub
deleted theorem Real.sin_sq_le_one
deleted theorem Real.sin_sub
deleted theorem Real.sin_zero
deleted theorem Real.sinh_add_cosh
deleted theorem Real.sinh_lt_cosh
deleted theorem Real.sinh_neg
deleted theorem Real.sinh_sub
deleted theorem Real.sinh_sub_cosh
deleted theorem Real.sinh_zero
deleted theorem Real.tan_mul_cos
deleted theorem Real.tan_neg
deleted theorem Real.tan_zero
deleted theorem Real.tanh_neg
deleted theorem Real.tanh_zero
deleted theorem Real.two_mul_cos_mul_cos
deleted theorem Real.two_mul_sin_mul_cos
deleted theorem Real.two_mul_sin_mul_sin
added theorem Complex.abs_exp
added def Complex.cos
added theorem Complex.cos_add
added theorem Complex.cos_add_cos
added theorem Complex.cos_add_mul_I
added theorem Complex.cos_add_sin_I
added theorem Complex.cos_conj
added theorem Complex.cos_eq
added theorem Complex.cos_mul_I
added theorem Complex.cos_neg
added theorem Complex.cos_ofReal_im
added theorem Complex.cos_ofReal_re
added theorem Complex.cos_sq'
added theorem Complex.cos_sq
added theorem Complex.cos_sub
added theorem Complex.cos_sub_cos
added theorem Complex.cos_sub_sin_I
added theorem Complex.cos_three_mul
added theorem Complex.cos_two_mul'
added theorem Complex.cos_two_mul
added theorem Complex.cos_zero
added def Complex.cosh
added theorem Complex.cosh_add
added theorem Complex.cosh_add_sinh
added theorem Complex.cosh_conj
added theorem Complex.cosh_mul_I
added theorem Complex.cosh_neg
added theorem Complex.cosh_ofReal_im
added theorem Complex.cosh_ofReal_re
added theorem Complex.cosh_sq
added theorem Complex.cosh_sub
added theorem Complex.cosh_sub_sinh
added theorem Complex.cosh_three_mul
added theorem Complex.cosh_two_mul
added theorem Complex.cosh_zero
added def Complex.cot
added theorem Complex.cot_conj
added theorem Complex.exp_add_mul_I
added theorem Complex.exp_im
added theorem Complex.exp_mul_I
added theorem Complex.exp_re
added theorem Complex.exp_sub_cosh
added theorem Complex.exp_sub_sinh
added theorem Complex.ofReal_cos
added theorem Complex.ofReal_cosh
added theorem Complex.ofReal_cot
added theorem Complex.ofReal_sin
added theorem Complex.ofReal_sinh
added theorem Complex.ofReal_tan
added theorem Complex.ofReal_tanh
added def Complex.sin
added theorem Complex.sin_add
added theorem Complex.sin_add_mul_I
added theorem Complex.sin_add_sin
added theorem Complex.sin_conj
added theorem Complex.sin_eq
added theorem Complex.sin_mul_I
added theorem Complex.sin_neg
added theorem Complex.sin_ofReal_im
added theorem Complex.sin_ofReal_re
added theorem Complex.sin_sq
added theorem Complex.sin_sub
added theorem Complex.sin_sub_sin
added theorem Complex.sin_three_mul
added theorem Complex.sin_two_mul
added theorem Complex.sin_zero
added def Complex.sinh
added theorem Complex.sinh_add
added theorem Complex.sinh_add_cosh
added theorem Complex.sinh_conj
added theorem Complex.sinh_mul_I
added theorem Complex.sinh_neg
added theorem Complex.sinh_ofReal_im
added theorem Complex.sinh_ofReal_re
added theorem Complex.sinh_sq
added theorem Complex.sinh_sub
added theorem Complex.sinh_sub_cosh
added theorem Complex.sinh_three_mul
added theorem Complex.sinh_two_mul
added theorem Complex.sinh_zero
added def Complex.tan
added theorem Complex.tan_conj
added theorem Complex.tan_mul_I
added theorem Complex.tan_mul_cos
added theorem Complex.tan_neg
added theorem Complex.tan_ofReal_im
added theorem Complex.tan_ofReal_re
added theorem Complex.tan_zero
added def Complex.tanh
added theorem Complex.tanh_conj
added theorem Complex.tanh_mul_I
added theorem Complex.tanh_neg
added theorem Complex.tanh_ofReal_im
added theorem Complex.tanh_ofReal_re
added theorem Complex.tanh_zero
added theorem Complex.two_cos
added theorem Complex.two_cosh
added theorem Complex.two_sin
added theorem Complex.two_sinh
added theorem Real.abs_cos_le_one
added theorem Real.abs_sin_le_one
added theorem Real.cos_abs
added theorem Real.cos_bound
added theorem Real.cos_le_one
added theorem Real.cos_neg
added theorem Real.cos_one_le
added theorem Real.cos_one_pos
added theorem Real.cos_pos_of_le_one
added theorem Real.cos_sq'
added theorem Real.cos_sq_add_sin_sq
added theorem Real.cos_sq_le_one
added theorem Real.cos_sub
added theorem Real.cos_two_neg
added theorem Real.cos_zero
added theorem Real.cosh_abs
added theorem Real.cosh_add_sinh
added theorem Real.cosh_eq
added theorem Real.cosh_neg
added theorem Real.cosh_pos
added theorem Real.cosh_sq'
added theorem Real.cosh_sub
added theorem Real.cosh_sub_sinh
added theorem Real.cosh_zero
added theorem Real.exp_sub_cosh
added theorem Real.exp_sub_sinh
added theorem Real.neg_one_le_cos
added theorem Real.neg_one_le_sin
added theorem Real.sin_bound
added theorem Real.sin_le_one
added theorem Real.sin_neg
added theorem Real.sin_sq
added theorem Real.sin_sq_le_one
added theorem Real.sin_sub
added theorem Real.sin_zero
added theorem Real.sinh_add_cosh
added theorem Real.sinh_lt_cosh
added theorem Real.sinh_neg
added theorem Real.sinh_sub
added theorem Real.sinh_sub_cosh
added theorem Real.sinh_zero
added theorem Real.tan_mul_cos
added theorem Real.tan_neg
added theorem Real.tan_zero
added theorem Real.tanh_neg
added theorem Real.tanh_zero