Metamath Proof Explorer


Table of Contents - 10.1.3. Iterated sums in a magma

The symbol is mostly used in the context of abelian groups. Therefore, it is usually called "group sum". It can be defined, however, in arbitrary magmas (then it should be called "iterated sum"). If the magma is not required to be commutative or associative, then the order of the summands and the order in which summations are done become important. If the magma is not unital, then one cannot define a meaningful empty sum. See Remark 2. in the comment for df-gsum.

  1. gsumvalx
  2. gsumval
  3. gsumpropd
  4. gsumpropd2lem
  5. gsumpropd2
  6. gsummgmpropd
  7. gsumress
  8. gsumval1
  9. gsum0
  10. gsumval2a
  11. gsumval2
  12. gsumsplit1r
  13. gsumprval
  14. gsumpr12val