Syntax Definition csm 4960

Description: Extend class notation with scalar multiplication on Hilbert space. In the literature scalar multiplication is usually indicated by juxtaposition, but we need an explicit symbol to prevent ambiguity.

Assertion

Ref	Expression
csm	class ·s

This syntax is primitive. The first axiom using it is ax-hvmulcl 4989.

metamath.org