Metamath Proof Explorer


Syntax definition cdsmm

Description: Class of module direct sum generator.

Ref Expression
Assertion cdsmm
class (+)m