Metamath Proof Explorer


Syntax definition cpm2mp

Description: Extend class notation with the transformation of a polynomial matrix into a polynomial over matrices.

Ref Expression
Assertion cpm2mp class pMatToMatPoly