Metamath Proof Explorer


Syntax definition ctimesr

Description: Introduce the operation of scalar multiplication.

Ref Expression
Assertion ctimesr
class .v