Metamath Proof Explorer


Syntax definition clinc

Description: Extend class notation with the operation constructing a linear combination (of vectors from a left module).

Ref Expression
Assertion clinc class linC