Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-28 07:29 01adfd65

View on Github →

chore(analysis/special_functions): add some @[simp] attrs (#9423) Add @[simp] attrs to real.sin_add_pi and similar lemmas.

Estimated changes

modified theorem real.cos_add_int_mul_two_pi
modified theorem real.cos_add_nat_mul_two_pi
modified theorem real.cos_add_pi
modified theorem real.cos_add_two_pi
modified theorem real.cos_int_mul_two_pi
modified theorem real.cos_int_mul_two_pi_sub
modified theorem real.cos_nat_mul_two_pi
modified theorem real.cos_nat_mul_two_pi_sub
modified theorem real.cos_pi_sub
modified theorem real.cos_sub_int_mul_two_pi
modified theorem real.cos_sub_nat_mul_two_pi
modified theorem real.cos_sub_pi
modified theorem real.cos_sub_two_pi
modified theorem real.cos_two_pi_sub
modified theorem real.sin_add_int_mul_two_pi
modified theorem real.sin_add_nat_mul_two_pi
modified theorem real.sin_add_pi
modified theorem real.sin_add_two_pi
modified theorem real.sin_int_mul_pi
modified theorem real.sin_int_mul_two_pi_sub
modified theorem real.sin_nat_mul_pi
modified theorem real.sin_nat_mul_two_pi_sub
modified theorem real.sin_pi_sub
modified theorem real.sin_sub_int_mul_two_pi
modified theorem real.sin_sub_nat_mul_two_pi
modified theorem real.sin_sub_pi
modified theorem real.sin_sub_two_pi
modified theorem real.sin_two_pi_sub