Metamath Proof Explorer


Syntax definition cuvc

Description: Class of basic unit vectors for an explicit free module.

Ref Expression
Assertion cuvc class unitVec