Commit 2025-10-06 14:25 d799b46e

View on Github →

feat(Positivity): add positivity extensions for NNReal.rpow and ENNReal.rpow (#29463)

Estimated changes

Modified Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean

added theorem ENNReal.rpow_zero_pos

added def Mathlib.Meta.Positivity.evalENNRealRpow

added def Mathlib.Meta.Positivity.evalNNRealRpow

added theorem NNReal.rpow_zero_pos

Modified MathlibTest/positivity.lean