Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-20 05:38 050b5a1b

View on Github →

feat(data/real/pi): Leibniz's series for pi (#4228) Freek No. 26

Estimated changes

Modified docs/100.yaml

Modified src/analysis/special_functions/exp_log.lean

added theorem real.tendsto_div_pow_mul_exp_add_at_top

added theorem real.tendsto_exp_nhds_0_nhds_1

added theorem real.tendsto_mul_exp_add_div_pow_at_top

Modified src/analysis/special_functions/pow.lean

added theorem real.log_rpow

added theorem tendsto_rpow_at_top

added theorem tendsto_rpow_div

added theorem tendsto_rpow_div_mul_add

added theorem tendsto_rpow_neg_at_top

added theorem tendsto_rpow_neg_div

Modified src/data/real/pi.lean

added theorem real.tendsto_sum_pi_div_four

Modified src/topology/algebra/monoid.lean

added theorem tendsto.const_mul

added theorem tendsto.mul_const

Modified src/topology/algebra/ordered.lean

added theorem tendsto_pow_at_top

added theorem tendsto_pow_neg_at_top