Metamath Proof Explorer


Syntax definition clnm

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

Ref Expression
Assertion clnm class LNoeM