Metamath Proof Explorer


Syntax definition cpid

Description: Class of principal ideal domains.

Ref Expression
Assertion cpid class PID