Discrete additive subgroup of a real vector space (source code)

= Discrete additive subgroup of a real vector space
{title2=$\Lambda=\mathbb Zv_1+\cdots+\mathbb Zv_r$}

A discrete additive <subgroup> of $\mathbb R^n$ is generated by real-linearly independent vectors. Indeed, isolation of zero gives uniform separation, so compact sets meet the <subgroup> finitely. Choose a real basis from the <subgroup> for its real span. Its <integer> span has finite index, since reduction into a compact fundamental parallelepiped gives finitely many <coset> representatives. The <structure theorem for finitely generated abelian groups> then gives a free <integer> basis, whose size is the dimension of the real span. Thus the <subgroup> is a <Euclidean lattice> in its span, although it need not have full rank in the ambient space.