Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-16 05:34 1cce6064

View on Github →

feat(analysis/special_functions/trigonometric): some lemmas (#4638) The following changes:

  • sin_sub_sin and friends (sum-to-product lemmas) moved from trigonometric to the earlier file exponential. (I think the distinction between the files is that trigonometric collects the facts that require either differentiation or the definition pi, whereas purely algebraic facts about trigonometry go in exponential? For example the double-angle formula is in exponential).
  • rewrite proof of cos_lt_cos_of_nonneg_of_le_pi_div_two to avoid dependence on cos_eq_one_iff_of_lt_of_lt (but not sure if the result is actually simpler, feel free to propose this be reverted)
  • some new explicit values of trig functions, cos (π / 3) and similar
  • correct a series of lemmas in the complex namespace that were stated for real arguments (presumably the author copy-pasted but forgot to rewrite)
  • lemmas sin_eq_zero_iff, cos_eq_cos_iff, sin_eq_sin_iff

Estimated changes

modified theorem complex.cos_add_pi
modified theorem complex.cos_add_pi_div_two
modified theorem complex.cos_add_two_pi
added theorem complex.cos_eq_cos_iff
modified theorem complex.cos_pi_div_two_sub
modified theorem complex.cos_pi_sub
modified theorem complex.cos_sub_pi_div_two
modified theorem complex.sin_add_pi
modified theorem complex.sin_add_pi_div_two
modified theorem complex.sin_add_two_pi
added theorem complex.sin_eq_sin_iff
modified theorem complex.sin_pi_div_two_sub
modified theorem complex.sin_pi_sub
modified theorem complex.sin_sub_pi_div_two
added theorem real.cos_eq_cos_iff
added theorem real.cos_pi_div_six
added theorem real.cos_pi_div_three
deleted theorem real.cos_sub_cos
added theorem real.sin_eq_sin_iff
added theorem real.sin_pi_div_six
added theorem real.sin_pi_div_three
deleted theorem real.sin_sub_sin
added theorem complex.cos_add_cos
added theorem complex.cos_sub_cos
added theorem complex.sin_sub_sin
added theorem real.cos_add_cos
added theorem real.cos_sub_cos
added theorem real.sin_sub_sin