Finitely generated module (source code)

= Finitely generated module

An $R$-module is finitely generated when there are finitely many elements $m_1,\ldots,m_r$ such that every element is an $R$-linear combination of them.