chore(analysis/special_functions/trigonometric/basic): move results a…

…bout derivatives to a new file (#10109) 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.
leanprover-community · Nov 2, 2021 · 70ed9dc · 70ed9dc
1 parent d43daf0
commit 70ed9dc
Show file tree

Hide file tree

Showing 6 changed files with 885 additions and 851 deletions.
diff --git a/src/analysis/special_functions/arsinh.lean b/src/analysis/special_functions/arsinh.lean
@@ -3,7 +3,7 @@ Copyright (c) 2020 James Arthur. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: James Arthur, Chris Hughes, Shing Tak Lam
 -/
-import analysis.special_functions.trigonometric.basic
+import analysis.special_functions.trigonometric.deriv
 import analysis.special_functions.log
 
 /-!