Metamath Proof Explorer


Syntax definition crglmod

Description: Extend class notation with the left module induced by a ring over itself.

Ref Expression
Assertion crglmod class ringLMod