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. For the usual textbook definition of a (left) ideal of a ring to be a subgroup of the additive group of the ring which is closed under left-multiplication by elements of the full ring, see dflidl2 . (Contributed by Stefan O'Rear, 31-Mar-2015)

Ref Expression
Assertion df-lidl
|- LIdeal = ( LSubSp o. ringLMod )

Detailed syntax breakdown

Step Hyp Ref Expression
0 clidl
 |-  LIdeal
1 clss
 |-  LSubSp
2 crglmod
 |-  ringLMod
3 1 2 ccom
 |-  ( LSubSp o. ringLMod )
4 0 3 wceq
 |-  LIdeal = ( LSubSp o. ringLMod )