Several utility theorems

[tirix]

This adds several utility theorems to my mathbox, and moves corresponding required theorems to main.

The two main theorems are:

• gsumpart, which rewrites a group sum as a double sum, grouping along a possibly infinite partition (but the sum is over a finite support, so the overall sum remains finite)
• gsumhashmul, which expresses a group sum by grouping by nonzero values, multiplied by the number of times those values appear in the sum.

So, nothing exciting in this PR, but some ground work which will hopefully be useful in the upcoming ones.

[tirix]

Thanks to @avekens for very relevant remarks, both are taken into account.