Commit 2020-06-03 16:19 ef6d8d9e

refactor(analysis/specific_limits): prove 0 < r → (1+r)^n→∞ for semirings (#2935)

• Add add_one_pow_unbounded_of_pos and tendsto_add_one_pow_at_top_at_top_of_pos assuming [linear_ordered_semiring α] [archimedean α].
• Rename tendsto_pow_at_top_at_top_of_gt_1 to tendsto_pow_at_top_at_top_of_one_lt, generalize to an archimedean ordered ring.
• Rename tendsto_pow_at_top_at_top_of_gt_1_nat to nat.tendsto_pow_at_top_at_top_of_one_lt.