Metamath Proof Explorer


Syntax definition clinco

Description: Extend class notation with the operation constructing a set of linear combinations (of vectors from a left module) with finite support.

Ref Expression
Assertion clinco class LinCo