Definition df-lidl 21343

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 dflidl2rng 21354 and dflidl2 21364. (Contributed by Stefan O'Rear, 31-Mar-2015.)

Assertion

Ref	Expression
df-lidl	⊢ LIdeal = (LSubSp ∘ ringLMod)

Detailed syntax breakdown of Definition df-lidl

Step	Hyp	Ref	Expression
1		clidl 21341	. 2 class LIdeal
2		clss 21063	. . 3 class LSubSp
3		crglmod 21304	. . 3 class ringLMod
4	2, 3	ccom 5664	. 2 class (LSubSp ∘ ringLMod)
5	1, 4	wceq 1569	1 wff LIdeal = (LSubSp ∘ ringLMod)

This definition is used by:  lidlval  21345