Metamath Proof Explorer


Syntax definition ccnfld

Description: Extend class notation with the field of complex numbers.

Ref Expression
Assertion ccnfld
class CCfld