arctan): put lemmas about derivatives into a new file (#10157)

Commit

4 years ago

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

Author

RemyDegenne

Parents

02100d81

mathlib d5d60719 - chore(analysis/special_functions/trigonometric/arctan): put lemmas about derivatives into a new file (#10157)

mathlib
d5d60719 - chore(analysis/special_functions/trigonometric/arctan): put lemmas about derivatives into a new file (#10157)