feat(analysis/special_functions): limit of x^s * exp(-x) for s real (#12540)
feat(analysis/special_functions): limit of x^s * exp(-x) for s real (#12540)



Co-authored-by: sgouezel <06bcd766296da4e7f3f1690c64fbdb3ee30e2f66@univ-rennes1.fr>

leanprover-community/mathlib,leanprover-community/mathlib