Metamath Proof Explorer


Syntax definition cza

Description: Extend class notation with the class of algebraic integers.

Ref Expression
Assertion cza
class _ZZ