Finite generation is preserved by module extensions (source code)

= Finite generation is preserved by module extensions
{title2=$N,\ M/N\text{ finitely generated}\implies M\text{ finitely generated}$}

If a <submodule> $N\subseteq M$ and the <quotient module> $M/N$ are <finitely generated modules>, then $M$ is a <finitely generated module>. Choose finitely many generators of $N$ and lift finitely many generators of $M/N$. For any $m\in M$, subtract an $R$-linear combination of the lifts to obtain an element of $N$, then express this using the generators of $N$. The union of the two finite lists generates $M$.