complex): put results about derivatives into a new file (#10156)

Commit

4 years ago

chore(analysis/special_functions/trigonometric/complex): put results about derivatives into a new file (#10156) Co-authored-by: RemyDegenne <remydegenne@gmail.com>

Author

RemyDegenne

Parents

62621659

mathlib adb5c2d6 - chore(analysis/special_functions/trigonometric/complex): put results about derivatives into a new file (#10156)

mathlib
adb5c2d6 - chore(analysis/special_functions/trigonometric/complex): put results about derivatives into a new file (#10156)