mathlib3
8f7ffec9 - chore(analysis/special_functions/trigonometric/inverse): move results about derivatives to a new file (#10110)

Commit
4 years ago
chore(analysis/special_functions/trigonometric/inverse): move results about derivatives to a new file (#10110) This is part of a refactor of the `analysis/special_functions` folder, in which I will isolate all lemmas about derivatives. The result will be a definition of Lp spaces that does not import derivatives. Co-authored-by: RemyDegenne <remydegenne@gmail.com>
Author
Parents
Loading