Given a (abelian) group $G$ and a family $\lbrace g_i \rbrace$ of elements of $G$ indexed by a set $I$, is there a notation for the elements $\sum_{i \in I} g_i$ in one of the many formalizations of group theory in the main library or in the AFP?

The ‘canonical’ formalisation of group theory is HOL-Algebra. Groups are written multiplicatively in HOL-Algebra, and the concept you are looking for is called `finprod`

in `HOL-Algebra.Finite_Product`

: `⨂⇘G⇙ i∈I. g i`

This is defined for any commutative monoid.

I tried to parse their code but I don't immediately see why they require the index set (named `A`

there) to be finite. What does prevent `A`

from being infinite?

If it's infinite, it might not even be well-defined.

You would need a topological group for that to even make sense

I don't think we have topological groups in HOL-Algebra

If you're not interested in abstract algebra but your groups are very "concrete", it might make more sense to define a type for them and just use the "normal" operations for indexed sums and products.

For infinite sums, it depends a bit on what kind of summation you want. If the summation order is fixed, there's `suminf`

. Otherwise I don't think we have terribly much, unfortunately.

But let's not get ahead of ourselves, what kind of objects are you trying to sum?

I realized tonight that I could express what I wanted without introducing these arbitrary sums of elements of an abelian group. So, my problem is solved, at least for now. Thanks for your help.

Last updated: Feb 27 2024 at 08:17 UTC