feat: port Analysis.SpecialFunctions.Pow.NNReal (#4161)

Co-authored-by: int-y1 <jason_yuen2007@hotmail.com>
leanprover-community · May 21, 2023 · 85b38a0 · 85b38a0
1 parent 9ef61a0
commit 85b38a0
Show file tree

Hide file tree

Showing 2 changed files with 877 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -466,6 +466,7 @@ import Mathlib.Analysis.SpecialFunctions.Log.Basic
 import Mathlib.Analysis.SpecialFunctions.Log.Monotone
 import Mathlib.Analysis.SpecialFunctions.Polynomials
 import Mathlib.Analysis.SpecialFunctions.Pow.Complex
+import Mathlib.Analysis.SpecialFunctions.Pow.NNReal
 import Mathlib.Analysis.SpecialFunctions.Pow.Real
 import Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
 import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic