Metamath Proof Explorer


Theorem lnrlnm

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

Ref Expression
Assertion lnrlnm A LNoeR ringLMod A LNoeM

Proof

Step Hyp Ref Expression
1 islnr A LNoeR A Ring ringLMod A LNoeM
2 1 simprbi A LNoeR ringLMod A LNoeM