Metamath Proof Explorer


Syntax definition clmhm

Description: Extend class notation with the generator of left module hom-sets.

Ref Expression
Assertion clmhm class LMHom