Metamath Proof Explorer


Syntax definition clmim

Description: The class of left module isomorphism sets.

Ref Expression
Assertion clmim class LMIso