HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Syntax Definition cns 8206
Description: Extend class notation with scalar multiplication in a normed complex vector space. In the literature scalar multiplication is usually indicated by juxtaposition, but we need an explicit symbol to prevent ambiguity.
Assertion
Ref Expression
cns class .s

See definition df-sm 8216 for more information.

Colors of variables: wff set class
Copyright terms: Public domain