Naming: geom_sum vs geom_series

Stream: general

[Eric Wieser]

We have docs#geom_series x n which is defined as ∑ i in range n, x ^ i. However, we then have a bunch of lemmas like docs#geom_sum_mul_add which are statements about geom_series even though they look like they should be statements about a hypothetical geom_sum.

Presumably we should eradicate one of these names for consistency; which is preferred?

cc @Paul van Wamelen, as your #6828 made me think about this.

[Eric Wieser]

Is geom_sum reserved for the lemmas that us a summation but not the geom_series definition?

[Johan Commelin]

I think geom_series should refer to the infinite sum, and geom_sum to the finite sum. So it looks like docs#geom_series should be renamed.