Theorem lnrlnm

Description: Left-Noetherian rings have Noetherian associated modules. (Contributed by Stefan O'Rear, 24-Jan-2015)

	Ref	Expression
Assertion	lnrlnm	$$⊢A\in \mathrm{LNoeR}\to \mathrm{ringLMod}\left(A\right)\in \mathrm{LNoeM}$$

Proof

Step	Hyp	Ref	Expression
1		islnr	$$⊢A\in \mathrm{LNoeR}\leftrightarrow \left(A\in \mathrm{Ring}\wedge \mathrm{ringLMod}\left(A\right)\in \mathrm{LNoeM}\right)$$
2	1	simprbi	$$⊢A\in \mathrm{LNoeR}\to \mathrm{ringLMod}\left(A\right)\in \mathrm{LNoeM}$$