Metamath Proof Explorer


Syntax definition cidom

Description: Class of integral domains.

Ref Expression
Assertion cidom
class IDomn