Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-11-30 16:23 343c54d6

View on Github →

feat(analysis/complex/exponential): limits of exp (#1744)

staging
exp div pow
cleanup
oops
better proof
cleanup
docstring
typo in docstring

Estimated changes

Modified src/analysis/complex/exponential.lean

modified theorem real.sin_gt_sub_cube

added theorem real.tendsto_exp_at_top

added theorem real.tendsto_exp_div_pow_at_top

added theorem real.tendsto_exp_neg_at_top_nhds_0

added theorem real.tendsto_pow_mul_exp_neg_at_top_nhds_0

Modified src/analysis/specific_limits.lean

added theorem tendsto_at_top_div

added theorem tendsto_at_top_mul_left'

added theorem tendsto_at_top_mul_left

added theorem tendsto_at_top_mul_right'

added theorem tendsto_at_top_mul_right

modified theorem tendsto_pow_at_top_at_top_of_gt_1