Metamath Proof Explorer


Syntax definition cim

Description: Extend class notation to include imaginary part of a complex number.

Ref Expression
Assertion cim class