Metamath Proof Explorer


Syntax definition clnr

Description: Extend class notation with the class of left Noetherian rings.

Ref Expression
Assertion clnr class LNoeR