Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit 70ed9dc

Browse files
committed
chore(analysis/special_functions/trigonometric/basic): move results about 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.
1 parent d43daf0 commit 70ed9dc

File tree

6 files changed

+885
-851
lines changed

6 files changed

+885
-851
lines changed

src/analysis/special_functions/arsinh.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2020 James Arthur. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: James Arthur, Chris Hughes, Shing Tak Lam
55
-/
6-
import analysis.special_functions.trigonometric.basic
6+
import analysis.special_functions.trigonometric.deriv
77
import analysis.special_functions.log
88

99
/-!

0 commit comments

Comments
 (0)