Metamath Proof Explorer

Syntax definition clpir

Description: Class of left principal ideal rings.

Ref Expression
Assertion clpir 
class LPIR