feat: port Analysis.SpecialFunctions.Pow.Deriv (#4689)

Co-authored-by: Moritz Firsching <firsching@google.com> Co-authored-by: Johan Commelin <johan@commelin.net>
leanprover-community · Jun 6, 2023 · a9359cb · a9359cb
1 parent 41086ad
commit a9359cb
Show file tree

Hide file tree

Showing 2 changed files with 631 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -640,6 +640,7 @@ import Mathlib.Analysis.SpecialFunctions.Polynomials
 import Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
 import Mathlib.Analysis.SpecialFunctions.Pow.Complex
 import Mathlib.Analysis.SpecialFunctions.Pow.Continuity
+import Mathlib.Analysis.SpecialFunctions.Pow.Deriv
 import Mathlib.Analysis.SpecialFunctions.Pow.NNReal
 import Mathlib.Analysis.SpecialFunctions.Pow.Real
 import Mathlib.Analysis.SpecialFunctions.Sqrt