MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cns Structured version   Visualization version   GIF version

Syntax Definition cns 28370
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.
Ref Expression
cns class ·𝑠OLD

See definition df-sm 28380 for more information.

Colors of variables: wff setvar class
  Copyright terms: Public domain W3C validator