Metamath Proof Explorer

Table of Contents - 21.20.7.16. Finite sums in monoids

UPDATE: a similar summation is already defined as df-gsum (although it mixes finite and infinite sums, which makes it harder to understand).

1. cfinsum
2. df-bj-finsum
3. bj-finsumval0