HomeHome Hilbert Space Explorer < Previous   Next >
Related theorems
Unicode version
Syntax Definition csm 8970
Description: Extend class notation with scalar multiplication in 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 .h
This syntax is primitive. The first axiom using it is ax-hfvmul 9023.
Colors of variables: wff set class
Copyright terms: Public domain