Commit 2023-05-31 19:45 af5eea30
View on Github →feat: positivity extension for Real.rpow (#4486)
This PR introduces a positivity extension for Real.rpow. It is located at the same place as the mathlib3 version, namely in Analysis/SpecialFunctions/Pow/Real.lean.
Note that the two tests I left commented out fail, but due to coercions from ℝ≥0∞ not working yet.