Theorem Real.rpow_le_rpow_of_exponent_nonpos

Modification history

2023-08-13 08:12
Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
feat: lemmas about monotonicity and asymptotics of `rpow` (#6140)
Added Real.rpow_le_rpow_of_exponent_nonposView on Github →