Metamath Proof Explorer

Syntax definition cpid

Description: Class of principal ideal domains.

Ref Expression
Assertion cpid 
class PID