Auxiliary theorems about group sums and polynomials
Auxiliary theorems about group sums and polynomials

main part:
- ~ ply1coe holds also for non-commutative rings
- theorems about gsum
- theorems about (coefficients of) polynomials
AV's Mathbox:
- new class symbols
- support of functions over the nonnegative integers
- theorems about gsum
- theorems about (coefficients of) polynomials
- theorems about matrices consisting of polynomials

metamath/set.mm,metamath/set.mm,metamath/set.mm