exponential): simplify proof of `tan_eq_sin_div_cos` (#5913)

Commit

4 years ago

refactor(data/complex/exponential): simplify proof of `tan_eq_sin_div_cos` (#5913) Co-authors: `lean-gptf`, Stanislas Polu Co-authored-by: Mario Carneiro <di.gama@gmail.com>

Author

Jesse Michael Han

Parents

e927930c

mathlib3 1688b3e8 - refactor(data/complex/exponential): simplify proof of `tan_eq_sin_div_cos` (#5913)

mathlib3
1688b3e8 - refactor(data/complex/exponential): simplify proof of `tan_eq_sin_div_cos` (#5913)