Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-10 21:44 f72734a3

View on Github →

chore(data/complex/exponential): add inv_one_add_tan_sq etc (#5299)

  • mark cos_sq_add_sin_sq and sin_sq_add_cos_sq as @[simp];
  • add lemmas representing sin x and cos x as functions of tan x.

Estimated changes

modified theorem complex.sin_sq_add_cos_sq
added theorem complex.tan_mul_cos
added theorem real.cos_sq_add_sin_sq
modified theorem real.sin_sq_add_cos_sq
added theorem real.tan_mul_cos