Database
BASIC LINEAR ALGEBRA
Vectors and free modules
Direct sum of left modules
cdsmm
Next ⟩
df-dsmm
Metamath Proof Explorer
Ascii
Structured
Syntax definition
cdsmm
Description:
Class of module direct sum generator.
Ref
Expression
Assertion
cdsmm
class
⊕
m