Mathlib v3 is deprecated. Go to Mathlib v4

Theorem real.tan_mul_cos

Modification history

2020-12-10 21:44

src/data/complex/exponential.lean

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

Added real.tan_mul_cos View on Github →