Theorem Real.rpow_lt_rpow_of_exponent_neg

Modification history

2025-10-28 13:23
Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
chore(Analysis/SpecialFunctions/Pow): deprecate `rpow_lt_rpow_of_exponent_neg` and `rpow_le_rpow_of_exponent_nonpos` (#28375)
Deleted Real.rpow_lt_rpow_of_exponent_negView on Github →
2023-08-13 08:12
Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
feat: lemmas about monotonicity and asymptotics of `rpow` (#6140)
Added Real.rpow_lt_rpow_of_exponent_negView on Github →