Theorem NNReal.rpow_zero_pos

Modification history

2025-10-06 14:25

Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean

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

Added NNReal.rpow_zero_pos View on Github →