Metamath Proof Explorer


Syntax definition cdmat

Description: Extend class notation for the algebra of diagonal matrices.

Ref Expression
Assertion cdmat class DMat