Description: Extend a finite group sum by padding outside with zeroes. (Contributed by Mario Carneiro, 24-Apr-2016) (Revised by AV, 31-May-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | gsumzcl.b | |
|
gsumzcl.0 | |
||
gsumzcl.z | |
||
gsumzcl.g | |
||
gsumzcl.a | |
||
gsumzcl.f | |
||
gsumzcl.c | |
||
gsumzres.s | |
||
gsumzres.w | |
||
Assertion | gsumzres | |