Database
REAL AND COMPLEX NUMBERS
Elementary real and complex functions
Real and imaginary parts; conjugate
cim
Next ⟩
df-cj
Metamath Proof Explorer
Ascii
Unicode
Syntax definition
cim
Description:
Extend class notation to include imaginary part of a complex number.
Ref
Expression
Assertion
cim
$${class}\Im $$