Theorem Real.rpow_zero_pos

Modification history

2023-05-31 19:45
Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
feat: `positivity` extension for `Real.rpow` (#4486) …
Added Real.rpow_zero_posView on Github →