Noetherianity from finite additive rank (source code)

= Noetherianity from finite additive rank

If a ring $R$ is finitely generated as an abelian group, then it is Noetherian. Every ideal is an additive subgroup of that finitely generated abelian group and is therefore generated by finitely many elements as an abelian group. The same elements generate it as an $R$-ideal because integer multiples are already scalar multiples by elements of $R$.