exp_deriv): generalize some lemmas about `complex.exp`, remove `*.cexp_real` (#13579)

Commit

3 years ago

feat(analysis/special_functions/exp_deriv): generalize some lemmas about `complex.exp`, remove `*.cexp_real` (#13579) Now we can use `*.cexp` instead of some previous `*.cexp_real` lemmas. - [x] depends on: #13575

Author

astrainfinita

Parents

570db888

mathlib3 e7386121 - feat(analysis/special_functions/exp_deriv): generalize some lemmas about `complex.exp`, remove `*.cexp_real` (#13579)

mathlib3
e7386121 - feat(analysis/special_functions/exp_deriv): generalize some lemmas about `complex.exp`, remove `*.cexp_real` (#13579)