chore(analysis/special_functions/pow): put lemmas about derivatives i…

…nto 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>
leanprover-community · Nov 12, 2021 · c45e70a · c45e70a
1 parent 75207e9
commit c45e70a
Show file tree

Hide file tree

Showing 6 changed files with 664 additions and 505 deletions.
diff --git a/archive/100-theorems-list/9_area_of_a_circle.lean b/archive/100-theorems-list/9_area_of_a_circle.lean
@@ -5,6 +5,7 @@ Authors: James Arthur, Benjamin Davidson, Andrew Souther
 -/
 import measure_theory.integral.interval_integral
 import analysis.special_functions.sqrt
+import analysis.special_functions.trigonometric.inverse_deriv
 
 /-!
 # Freek № 9: The Area of a Circle

diff --git a/src/analysis/complex/polynomial.lean b/src/analysis/complex/polynomial.lean
@@ -5,6 +5,7 @@ Authors: Chris Hughes
 -/
 import analysis.special_functions.pow
 import field_theory.is_alg_closed.basic
+import topology.algebra.polynomial
 
 /-!
 # The fundamental theorem of algebra

diff --git a/src/analysis/convex/specific_functions.lean b/src/analysis/convex/specific_functions.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov, Sébastien Gouëzel
 -/
 import analysis.calculus.mean_value
-import analysis.special_functions.pow
+import analysis.special_functions.pow_deriv
 
 /-!
 # Collection of convex functions