 Discrete additive subgroup of a real vector space

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.