Metamath Proof Explorer


Syntax definition cgsu

Description: Extend class notation to include finitely supported group sums.

Ref Expression
Assertion cgsu
class gsum