Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-14 21:50 4a8ce41e

View on Github →

feat(analysis/special_functions/trigonometric): facts about periodic trigonometric functions (#7841) I use the periodicity API that I added in #7572 to write lemmas about sine (real and complex), cosine (real and complex), tangent (real and complex), and the exponential function (complex only).

Estimated changes

added theorem complex.cos_periodic
added theorem complex.cos_sub_pi
added theorem complex.cos_sub_two_pi
added theorem complex.cos_two_pi_sub
added theorem complex.exp_periodic
added theorem complex.sin_periodic
added theorem complex.sin_sub_pi
added theorem complex.sin_sub_two_pi
added theorem complex.sin_two_pi_sub
added theorem complex.tan_add_pi
added theorem complex.tan_nat_mul_pi
added theorem complex.tan_periodic
added theorem complex.tan_pi_sub
added theorem complex.tan_sub_pi
added theorem real.cos_antiperiodic
added theorem real.cos_periodic
added theorem real.cos_two_pi_sub
added theorem real.sin_antiperiodic
added theorem real.sin_periodic
added theorem real.sin_sub_pi
added theorem real.sin_two_pi_sub
added theorem real.tan_add_pi
added theorem real.tan_nat_mul_pi
added theorem real.tan_periodic
added theorem real.tan_pi_sub
added theorem real.tan_sub_pi