Finite-module extension preserves Noetherianity (source code)

= Finite-module extension preserves Noetherianity

Suppose $A\subseteq B$ are unital <rings> and $B$ is a <finitely generated module> over $A$ on the right. If $A$ is a <right Noetherian ring>, then $B_A$ is a <Noetherian module>. Every <right ideal> of $B$ is an $A$-<submodule>, hence has finitely many generators over $A$; these also generate it over $B$. Thus $B$ is a <right Noetherian ring>. The same argument works on the left under the corresponding hypotheses. Finite-index <group ring> extensions give an important example, using coset representatives as a finite module basis.