Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-27 04:20 a4b92a3f

View on Github →

refactor(analysis/special_functions/trigonometric): split file (#9340) Another mammoth file, cut into several pieces.

Estimated changes

added theorem complex.arg_I
added theorem complex.arg_eq_arg_iff
added theorem complex.arg_eq_pi_iff
added theorem complex.arg_le_pi
added theorem complex.arg_neg_I
added theorem complex.arg_neg_one
added theorem complex.arg_one
added theorem complex.arg_real_mul
added theorem complex.arg_zero
added theorem complex.cos_arg
added theorem complex.ext_abs_arg
added theorem complex.neg_pi_lt_arg
added theorem complex.sin_arg
added theorem complex.tan_arg
added theorem complex.exp_eq_one_iff
added theorem complex.exp_log
added theorem complex.log_I
added theorem complex.log_exp
added theorem complex.log_im
added theorem complex.log_im_le_pi
added theorem complex.log_neg_I
added theorem complex.log_neg_one
added theorem complex.log_of_real_re
added theorem complex.log_one
added theorem complex.log_re
added theorem complex.log_zero
added theorem complex.of_real_log
added theorem complex.range_exp
added theorem continuous.clog
added theorem continuous_at.clog
added theorem continuous_on.clog
added theorem differentiable.clog
added theorem differentiable_at.clog
added theorem differentiable_on.clog
added theorem filter.tendsto.clog
added theorem has_deriv_at.clog
added theorem has_fderiv_at.clog
added theorem deriv_arctan
added theorem deriv_within_arctan
added theorem differentiable.arctan
added theorem fderiv_arctan
added theorem fderiv_within_arctan
added theorem has_deriv_at.arctan
added theorem has_fderiv_at.arctan
added theorem real.arcsin_eq_arctan
added theorem real.arctan_eq_arcsin
added theorem real.arctan_mem_Ioo
added theorem real.arctan_neg
added theorem real.arctan_one
added theorem real.arctan_tan
added theorem real.arctan_zero
added theorem real.continuous_arctan
added theorem real.continuous_at_tan
added theorem real.continuous_on_tan
added theorem real.continuous_tan
added theorem real.cos_arctan
added theorem real.cos_arctan_pos
added theorem real.cos_sq_arctan
added theorem real.deriv_arctan
added theorem real.deriv_tan
added theorem real.has_deriv_at_tan
added theorem real.image_tan_Ioo
added theorem real.sin_arctan
added theorem real.surj_on_tan
added theorem real.tan_add'
added theorem real.tan_add
added theorem real.tan_arctan
added theorem real.tan_eq_zero_iff
added theorem real.tan_ne_zero_iff
added theorem real.tan_surjective
added theorem real.tan_two_mul
added theorem times_cont_diff.arctan
deleted theorem complex.arg_I
deleted theorem complex.arg_eq_arg_iff
deleted theorem complex.arg_eq_pi_iff
deleted theorem complex.arg_le_pi
deleted theorem complex.arg_neg_I
deleted theorem complex.arg_neg_one
deleted theorem complex.arg_one
deleted theorem complex.arg_real_mul
deleted theorem complex.arg_zero
deleted theorem complex.continuous_at_tan
deleted theorem complex.continuous_on_tan
deleted theorem complex.continuous_tan
deleted theorem complex.cos_arg
deleted theorem complex.cos_eq_cos_iff
deleted theorem complex.cos_eq_zero_iff
deleted theorem complex.cos_ne_zero_iff
deleted theorem complex.cos_surjective
deleted theorem complex.deriv_tan
deleted theorem complex.exists_pow_nat_eq
deleted theorem complex.exp_eq_one_iff
deleted theorem complex.exp_log
deleted theorem complex.ext_abs_arg
deleted theorem complex.has_deriv_at_tan
deleted theorem complex.log_I
deleted theorem complex.log_exp
deleted theorem complex.log_im
deleted theorem complex.log_im_le_pi
deleted theorem complex.log_neg_I
deleted theorem complex.log_neg_one
deleted theorem complex.log_of_real_re
deleted theorem complex.log_one
deleted theorem complex.log_re
deleted theorem complex.log_zero
deleted theorem complex.neg_pi_lt_arg
deleted theorem complex.neg_pi_lt_log_im
deleted theorem complex.of_real_log
deleted theorem complex.range_cos
deleted theorem complex.range_exp
deleted theorem complex.range_sin
deleted theorem complex.sin_arg
deleted theorem complex.sin_eq_sin_iff
deleted theorem complex.sin_eq_zero_iff
deleted theorem complex.sin_ne_zero_iff
deleted theorem complex.sin_surjective
deleted theorem complex.tan_add'
deleted theorem complex.tan_add
deleted theorem complex.tan_add_mul_I
deleted theorem complex.tan_arg
deleted theorem complex.tan_eq
deleted theorem complex.tan_eq_zero_iff
deleted theorem complex.tan_ne_zero_iff
deleted theorem complex.tan_two_mul
deleted theorem complex.two_pi_I_ne_zero
deleted theorem continuous.clog
deleted theorem continuous_at.clog
deleted theorem continuous_on.clog
deleted theorem continuous_within_at.clog
deleted theorem deriv_arctan
deleted theorem deriv_within_arctan
deleted theorem differentiable.arctan
deleted theorem differentiable.clog
deleted theorem differentiable_at.arctan
deleted theorem differentiable_at.clog
deleted theorem differentiable_on.arctan
deleted theorem differentiable_on.clog
deleted theorem fderiv_arctan
deleted theorem fderiv_within_arctan
deleted theorem filter.tendsto.clog
deleted theorem has_deriv_at.arctan
deleted theorem has_deriv_at.clog
deleted theorem has_deriv_within_at.clog
deleted theorem has_fderiv_at.arctan
deleted theorem has_fderiv_at.clog
deleted theorem has_fderiv_within_at.clog
deleted theorem has_strict_deriv_at.clog
deleted theorem has_strict_fderiv_at.clog
deleted theorem real.arccos_cos
deleted theorem real.arccos_eq_pi
deleted theorem real.arccos_eq_pi_div_two
deleted theorem real.arccos_eq_zero
deleted theorem real.arccos_inj
deleted theorem real.arccos_inj_on
deleted theorem real.arccos_le_pi
deleted theorem real.arccos_neg
deleted theorem real.arccos_neg_one
deleted theorem real.arccos_nonneg
deleted theorem real.arccos_one
deleted theorem real.arccos_zero
deleted theorem real.arcsin_eq_arctan
deleted theorem real.arcsin_eq_iff_eq_sin
deleted theorem real.arcsin_eq_of_sin_eq
deleted theorem real.arcsin_eq_pi_div_two
deleted theorem real.arcsin_eq_zero_iff
deleted theorem real.arcsin_inj
deleted theorem real.arcsin_le_iff_le_sin
deleted theorem real.arcsin_le_pi_div_two
deleted theorem real.arcsin_lt_iff_lt_sin
deleted theorem real.arcsin_lt_pi_div_two
deleted theorem real.arcsin_lt_zero
deleted theorem real.arcsin_mem_Icc
deleted theorem real.arcsin_neg
deleted theorem real.arcsin_neg_one
deleted theorem real.arcsin_nonneg
deleted theorem real.arcsin_nonpos
deleted theorem real.arcsin_of_le_neg_one
deleted theorem real.arcsin_of_one_le
deleted theorem real.arcsin_one
deleted theorem real.arcsin_pos
deleted theorem real.arcsin_proj_Icc
deleted theorem real.arcsin_sin'
deleted theorem real.arcsin_sin
deleted theorem real.arcsin_zero
deleted theorem real.arctan_eq_arcsin
deleted theorem real.arctan_eq_of_tan_eq
deleted theorem real.arctan_lt_pi_div_two
deleted theorem real.arctan_mem_Ioo
deleted theorem real.arctan_neg
deleted theorem real.arctan_one
deleted theorem real.arctan_tan
deleted theorem real.arctan_zero
deleted theorem real.continuous_arccos
deleted theorem real.continuous_arcsin
deleted theorem real.continuous_arctan
deleted theorem real.continuous_at_arcsin
deleted theorem real.continuous_at_arctan
deleted theorem real.continuous_at_tan
deleted theorem real.continuous_on_tan
deleted theorem real.continuous_tan
deleted theorem real.cos_arccos
deleted theorem real.cos_arcsin
deleted theorem real.cos_arcsin_nonneg
deleted theorem real.cos_arctan
deleted theorem real.cos_arctan_pos
deleted theorem real.cos_eq_cos_iff
deleted theorem real.cos_eq_zero_iff
deleted theorem real.cos_ne_zero_iff
deleted theorem real.cos_sq_arctan
deleted theorem real.deriv_arccos
deleted theorem real.deriv_arcsin
deleted theorem real.deriv_arcsin_aux
deleted theorem real.deriv_arctan
deleted theorem real.deriv_tan
deleted theorem real.has_deriv_at_arccos
deleted theorem real.has_deriv_at_arcsin
deleted theorem real.has_deriv_at_arctan
deleted theorem real.has_deriv_at_tan
deleted theorem real.image_tan_Ioo
deleted theorem real.inj_on_arcsin
deleted theorem real.le_arcsin_iff_sin_le
deleted theorem real.lt_arcsin_iff_sin_lt
deleted theorem real.maps_to_sin_Ioo
deleted theorem real.monotone_arcsin
deleted theorem real.pi_div_two_eq_arcsin
deleted theorem real.pi_div_two_le_arcsin
deleted theorem real.range_arcsin
deleted theorem real.sin_arccos
deleted theorem real.sin_arcsin'
deleted theorem real.sin_arcsin
deleted theorem real.sin_arctan
deleted theorem real.sin_eq_sin_iff
deleted theorem real.surj_on_tan
deleted theorem real.tan_add'
deleted theorem real.tan_add
deleted theorem real.tan_arctan
deleted theorem real.tan_eq_zero_iff
deleted theorem real.tan_ne_zero_iff
deleted def real.tan_order_iso
deleted theorem real.tan_surjective
deleted theorem real.tan_two_mul
deleted theorem real.zero_eq_arcsin_iff
deleted theorem times_cont_diff.arctan
deleted theorem times_cont_diff_at.arctan
deleted theorem times_cont_diff_on.arctan
added theorem complex.continuous_tan
added theorem complex.cos_eq_cos_iff
added theorem complex.cos_surjective
added theorem complex.deriv_tan
added theorem complex.range_cos
added theorem complex.range_sin
added theorem complex.sin_eq_sin_iff
added theorem complex.sin_surjective
added theorem complex.tan_add'
added theorem complex.tan_add
added theorem complex.tan_add_mul_I
added theorem complex.tan_eq
added theorem complex.tan_two_mul
added theorem real.cos_eq_cos_iff
added theorem real.cos_eq_zero_iff
added theorem real.cos_ne_zero_iff
added theorem real.sin_eq_sin_iff
added theorem real.arccos_cos
added theorem real.arccos_eq_pi
added theorem real.arccos_eq_zero
added theorem real.arccos_inj
added theorem real.arccos_inj_on
added theorem real.arccos_le_pi
added theorem real.arccos_neg
added theorem real.arccos_neg_one
added theorem real.arccos_nonneg
added theorem real.arccos_one
added theorem real.arccos_zero
added theorem real.arcsin_inj
added theorem real.arcsin_lt_zero
added theorem real.arcsin_mem_Icc
added theorem real.arcsin_neg
added theorem real.arcsin_neg_one
added theorem real.arcsin_nonneg
added theorem real.arcsin_nonpos
added theorem real.arcsin_of_one_le
added theorem real.arcsin_one
added theorem real.arcsin_pos
added theorem real.arcsin_proj_Icc
added theorem real.arcsin_sin'
added theorem real.arcsin_sin
added theorem real.arcsin_zero
added theorem real.continuous_arccos
added theorem real.continuous_arcsin
added theorem real.cos_arccos
added theorem real.cos_arcsin
added theorem real.cos_arcsin_nonneg
added theorem real.deriv_arccos
added theorem real.deriv_arcsin
added theorem real.deriv_arcsin_aux
added theorem real.inj_on_arcsin
added theorem real.maps_to_sin_Ioo
added theorem real.monotone_arcsin
added theorem real.range_arcsin
added theorem real.sin_arccos
added theorem real.sin_arcsin'
added theorem real.sin_arcsin