Theorem lnrring

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

	Ref	Expression
Assertion	lnrring	$$⊢A\in \mathrm{LNoeR}\to A\in \mathrm{Ring}$$

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	simplbi	$$⊢A\in \mathrm{LNoeR}\to A\in \mathrm{Ring}$$