Zulip Chat Archive

Stream: general

Topic: Naming: geom_sum vs geom_series


Eric Wieser (Mar 23 2021 at 11:59):

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 (Mar 23 2021 at 12:00):

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

Johan Commelin (Mar 23 2021 at 12:34):

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.


Last updated: Dec 20 2023 at 11:08 UTC