Metamath Proof Explorer

Syntax definition cfinsum

Description: Syntax for the class "finite summation in monoids".

Ref Expression
Assertion cfinsum class FinSum