Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-10-17 09:25 b5cd9746

View on Github →

feat(*): trigonometric functions: exp, log, sin, cos, tan, sinh, cosh, tanh, pi, arcsin, argcos, arg (#386)

  • floor_ring now is parameterized on a linear_ordered_ring instead of extending it.

Estimated changes

added theorem sub_floor_div_mul_lt
added theorem inv_pow'
added theorem pow_le_one
added theorem div_le_div_of_le_left
added theorem one_le_inv
added theorem mul_le_of_le_one_left
added theorem mul_le_of_le_one_right
added theorem one_lt_mul_of_le_of_lt
added theorem one_lt_mul_of_lt_of_le
added theorem complex.continuous_im
deleted theorem complex.continuous_mul
added theorem complex.continuous_re
added theorem complex.arg_I
added theorem complex.arg_eq_arg_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.continuous_cos
added theorem complex.continuous_exp
added theorem complex.continuous_sin
added theorem complex.continuous_tan
added theorem complex.cos_add_pi
added theorem complex.cos_add_two_pi
added theorem complex.cos_arg
added theorem complex.cos_pi
added theorem complex.cos_pi_div_two
added theorem complex.cos_pi_sub
added theorem complex.cos_two_pi
added theorem complex.exp_log
added theorem complex.ext_abs_arg
added theorem complex.log_I
added theorem complex.log_exp
added theorem complex.log_im
added theorem complex.log_neg_I
added theorem complex.log_neg_one
added theorem complex.log_one
added theorem complex.log_re
added theorem complex.log_zero
added theorem complex.neg_pi_lt_arg
added theorem complex.of_real_log
added theorem complex.sin_add_pi
added theorem complex.sin_add_two_pi
added theorem complex.sin_arg
added theorem complex.sin_int_mul_pi
added theorem complex.sin_nat_mul_pi
added theorem complex.sin_pi
added theorem complex.sin_pi_div_two
added theorem complex.sin_pi_sub
added theorem complex.sin_two_pi
added theorem complex.tan_arg
added theorem real.arccos_cos
added theorem real.arccos_inj
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_neg
added theorem real.arcsin_neg_one
added theorem real.arcsin_nonneg
added theorem real.arcsin_nonpos
added theorem real.arcsin_one
added theorem real.arcsin_pos
added theorem real.arcsin_sin
added theorem real.arcsin_zero
added theorem real.arctan_neg
added theorem real.arctan_tan
added theorem real.arctan_zero
added theorem real.continuous_cos
added theorem real.continuous_cosh
added theorem real.continuous_exp
added theorem real.continuous_sin
added theorem real.continuous_sinh
added theorem real.continuous_tan
added theorem real.cos_add_pi
added theorem real.cos_add_two_pi
added theorem real.cos_arccos
added theorem real.cos_arcsin
added theorem real.cos_arcsin_nonneg
added theorem real.cos_arctan
added theorem real.cos_eq_one_iff
added theorem real.cos_pi
added theorem real.cos_pi_div_two
added theorem real.cos_pi_sub
added theorem real.cos_two_pi
added theorem real.exists_sin_eq
added theorem real.exp_log
added theorem real.log_exp
added theorem real.log_one
added theorem real.log_zero
added theorem real.one_le_pi_div_two
added theorem real.pi_div_two_le_two
added theorem real.pi_div_two_pos
added theorem real.pi_le_four
added theorem real.pi_pos
added theorem real.sin_add_pi
added theorem real.sin_add_two_pi
added theorem real.sin_arccos
added theorem real.sin_arcsin
added theorem real.sin_arctan
added theorem real.sin_eq_zero_iff
added theorem real.sin_int_mul_pi
added theorem real.sin_nat_mul_pi
added theorem real.sin_pi
added theorem real.sin_pi_div_two
added theorem real.sin_pi_sub
added theorem real.sin_two_pi
added theorem real.tan_arctan
added theorem real.tan_surjective
added theorem real.two_le_pi
added theorem real.two_pi_pos
deleted theorem real.continuous_mul
added theorem complex.I_mul_I
added theorem complex.abs_cast_nat
added theorem complex.abs_two
added theorem complex.bit0_im
added theorem complex.bit0_re
added theorem complex.bit1_im
added theorem complex.bit1_re
added theorem complex.conj_neg_I
added theorem complex.conj_pow
added theorem complex.conj_sub
added theorem complex.conj_two
added theorem complex.is_cau_seq_abs
added theorem complex.lim_abs
added theorem complex.lim_add
added theorem complex.lim_conj
added theorem complex.lim_const
added theorem complex.lim_inv
added theorem complex.lim_mul
added theorem complex.lim_mul_lim
added theorem complex.lim_neg
added theorem complex.norm_sq_eq_abs
added theorem complex.of_real_pow
modified theorem complex.of_real_zero
added theorem abv_sum_le_sum_abv
added theorem cauchy_product
added def complex.cos
added theorem complex.cos_add
added theorem complex.cos_conj
added theorem complex.cos_neg
added theorem complex.cos_of_real_im
added theorem complex.cos_of_real_re
added theorem complex.cos_sub
added theorem complex.cos_two_mul
added theorem complex.cos_zero
added def complex.cosh
added theorem complex.cosh_add
added theorem complex.cosh_conj
added theorem complex.cosh_neg
added theorem complex.cosh_sub
added theorem complex.cosh_zero
added def complex.exp'
added def complex.exp
added theorem complex.exp_add
added theorem complex.exp_add_mul_I
added theorem complex.exp_bound
added theorem complex.exp_conj
added theorem complex.exp_mul_I
added theorem complex.exp_ne_zero
added theorem complex.exp_neg
added theorem complex.exp_of_real_im
added theorem complex.exp_of_real_re
added theorem complex.exp_sub
added theorem complex.exp_zero
added theorem complex.is_cau_abs_exp
added theorem complex.is_cau_exp
added theorem complex.of_real_cos
added theorem complex.of_real_cosh
added theorem complex.of_real_exp
added theorem complex.of_real_sin
added theorem complex.of_real_sinh
added theorem complex.of_real_tan
added theorem complex.of_real_tanh
added def complex.sin
added theorem complex.sin_add
added theorem complex.sin_conj
added theorem complex.sin_neg
added theorem complex.sin_of_real_im
added theorem complex.sin_of_real_re
added theorem complex.sin_sub
added theorem complex.sin_two_mul
added theorem complex.sin_zero
added def complex.sinh
added theorem complex.sinh_add
added theorem complex.sinh_conj
added theorem complex.sinh_neg
added theorem complex.sinh_sub
added theorem complex.sinh_zero
added def complex.tan
added theorem complex.tan_conj
added theorem complex.tan_neg
added theorem complex.tan_of_real_im
added theorem complex.tan_of_real_re
added theorem complex.tan_zero
added def complex.tanh
added theorem complex.tanh_conj
added theorem complex.tanh_neg
added theorem complex.tanh_zero
added theorem geo_sum_eq
added theorem geo_sum_inv_eq
added theorem is_cau_geo_series
added theorem is_cau_of_mono_bounded
added theorem real.abs_cos_le_one
added theorem real.abs_exp
added theorem real.abs_sin_le_one
added def real.cos
added theorem real.cos_add
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_sub
added theorem real.cos_two_mul
added theorem real.cos_two_neg
added theorem real.cos_zero
added def real.cosh
added theorem real.cosh_add
added theorem real.cosh_neg
added theorem real.cosh_sub
added theorem real.cosh_zero
added def real.exp
added theorem real.exp_add
added theorem real.exp_injective
added theorem real.exp_le_exp
added theorem real.exp_lt_exp
added theorem real.exp_ne_zero
added theorem real.exp_neg
added theorem real.exp_pos
added theorem real.exp_sub
added theorem real.exp_zero
added theorem real.neg_one_le_cos
added theorem real.neg_one_le_sin
added theorem real.one_le_exp
added def real.sin
added theorem real.sin_add
added theorem real.sin_bound
added theorem real.sin_le_one
added theorem real.sin_neg
added theorem real.sin_sub
added theorem real.sin_two_mul
added theorem real.sin_zero
added def real.sinh
added theorem real.sinh_add
added theorem real.sinh_neg
added theorem real.sinh_sub
added theorem real.sinh_zero
added def real.tan
added theorem real.tan_neg
added theorem real.tan_zero
added def real.tanh
added theorem real.tanh_neg
added theorem real.tanh_zero
added theorem series_ratio_test
added theorem sum_range_diag_flip
added theorem int.cast_two
added theorem nat.cast_two
added theorem real.le_lim
added theorem real.lim_le
added theorem real.lim_lt
added theorem real.lt_lim
added theorem cau_seq.le_of_eq_of_le
added theorem cau_seq.le_of_exists
added theorem cau_seq.le_of_le_of_eq