Commit 2025-10-28 13:23 e6fe7e4b

View on Github →

chore(Analysis/SpecialFunctions/Pow): deprecate rpow_lt_rpow_of_exponent_neg and rpow_le_rpow_of_exponent_nonpos (#28375)

Estimated changes

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

deleted theorem Real.rpow_le_rpow_of_exponent_nonpos

deleted theorem Real.rpow_lt_rpow_of_exponent_neg

Modified Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean

Modified Mathlib/Computability/AkraBazzi/SumTransform.lean