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

Commit c45e70a

Browse files
committed
chore(analysis/special_functions/pow): put lemmas about derivatives into a new file (#10153)
In order to keep results about continuity of the power function in the original file, we prove some continuity results directly (these were previously proved using derivatives). Co-authored-by: RemyDegenne <remydegenne@gmail.com>
1 parent 75207e9 commit c45e70a

File tree

6 files changed

+664
-505
lines changed

6 files changed

+664
-505
lines changed

archive/100-theorems-list/9_area_of_a_circle.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ Authors: James Arthur, Benjamin Davidson, Andrew Souther
55
-/
66
import measure_theory.integral.interval_integral
77
import analysis.special_functions.sqrt
8+
import analysis.special_functions.trigonometric.inverse_deriv
89

910
/-!
1011
# Freek № 9: The Area of a Circle

src/analysis/complex/polynomial.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ Authors: Chris Hughes
55
-/
66
import analysis.special_functions.pow
77
import field_theory.is_alg_closed.basic
8+
import topology.algebra.polynomial
89

910
/-!
1011
# The fundamental theorem of algebra

src/analysis/convex/specific_functions.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Yury Kudryashov, Sébastien Gouëzel
55
-/
66
import analysis.calculus.mean_value
7-
import analysis.special_functions.pow
7+
import analysis.special_functions.pow_deriv
88

99
/-!
1010
# Collection of convex functions

0 commit comments

Comments
 (0)