Metamath Proof Explorer


Syntax definition caz

Description: Extend class notation with the adjunctions of a complex number to the ring of integers.

Ref Expression
Assertion caz class Z[]