Given a (abelian) group and a family of elements of indexed by a set , is there a notation for the elements 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
⨂⇘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: Sep 22 2023 at 12:28 UTC