Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2022-03-11 08:22
1326aa7c
View on Github →
feat(analysis/special_functions): limit of x^s * exp(-x) for s real (
#12540
)
Estimated changes
Modified
src/analysis/special_functions/pow.lean
added
theorem
tendsto_exp_div_rpow_at_top
added
theorem
tendsto_exp_mul_div_rpow_at_top
added
theorem
tendsto_rpow_mul_exp_neg_mul_at_top_nhds_0