Metamath Proof Explorer


Syntax definition czr

Description: Integral elements of a ring.

Ref Expression
Assertion czr class ℤRing