Commit 2020-05-13 01:57 cbffb34c

feat(analysis/specific_limits): more geometric series (#2658) Currently, the sum of a geometric series is only known for real numbers in [0,1). We prove it for any element of a normed field with norm < 1, and specialize it to real numbers in (-1, 1). Some lemmas in analysis/specific_limits are also moved around (but their content is not changed) to get a better organization of this file.