Metamath Proof Explorer


Syntax definition ctimesr

Description: Introduce the operation of scalar multiplication.

Ref Expression
Assertion ctimesr class v