Countability of countably generated abelian groups (source code)

= Countability of countably generated abelian groups

A countably generated <abelian group> is a <countable set>. Given generators $g_1,g_2,\ldots$, every element is $\sum_{j=1}^ma_jg_j$ for some $m$ and some $a_j\in\mathbb Z$. For each fixed $m$, this is the image of a finite <cartesian product> of copies of the <countable set> $\mathbb Z$; taking a <countable union of countable sets> proves the assertion. The same proof works for a <module> generated by a <countable set> over any countable <ring>.