Mathlib Changelog
v4
Changelog
About
Github
Theorem
tendsto_rpow_neg_nhdsGT_zero
Modification history
2025-11-28 10:54
Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean
feat(Analysis): generalize `Real.deriv_rpow_const` and prove iteration version (#32196) …
Added
tendsto_rpow_neg_nhdsGT_zero
View on Github →