Metamath Proof Explorer


Syntax definition cdsmm

Description: Class of module direct sum generator.

Ref Expression
Assertion cdsmm class m