Commit 2020-09-06 11:28 fabf34f4

View on Github →

feat(analysis/special_functions/trigonometric): Added lemmas for deriv of tan (#3746) I added lemmas for the derivative of the tangent function in both the complex and real namespaces. I also corrected two typos in comment lines.

Estimated changes

Modified src/analysis/special_functions/trigonometric.lean

added theorem complex.continuous_on_tan

modified theorem complex.continuous_tan

added theorem complex.cos_eq_zero_iff

added theorem complex.cos_ne_zero_iff

added theorem complex.deriv_tan

added theorem complex.differentiable_at_tan

added theorem complex.exp_pi_mul_I

added theorem complex.has_deriv_at_tan

added theorem real.continuous_on_tan

modified theorem real.continuous_tan

modified theorem real.cos_eq_zero_iff

modified theorem real.cos_ne_zero_iff

added theorem real.cos_nonneg_of_mem_Icc

deleted theorem real.cos_nonneg_of_neg_pi_div_two_le_of_le_pi_div_two

added theorem real.cos_pos_of_mem_Ioo

deleted theorem real.cos_pos_of_neg_pi_div_two_lt_of_lt_pi_div_two

added theorem real.deriv_tan

added theorem real.deriv_tan_of_mem_Ioo

added theorem real.differentiable_at_tan

added theorem real.differentiable_at_tan_of_mem_Ioo

added theorem real.has_deriv_at_tan

added theorem real.has_deriv_at_tan_of_mem_Ioo