Metamath Proof Explorer


Definition df-lidl

Description: Define the class of left ideals of a given ring. An ideal is a submodule of the ring viewed as a module over itself. (Contributed by Stefan O'Rear, 31-Mar-2015)

Ref Expression
Assertion df-lidl LIdeal = LSubSp ringLMod

Detailed syntax breakdown

Step Hyp Ref Expression
0 clidl class LIdeal
1 clss class LSubSp
2 crglmod class ringLMod
3 1 2 ccom class LSubSp ringLMod
4 0 3 wceq wff LIdeal = LSubSp ringLMod