There is a statement which I have taken for granted for a long time but not able to formally prove it
How to formally prove that an abelian group $A$ $\mathbb Z$-spanned by $k$ linearly independent vectors $v_1,\cdots, v_k$ in $\mathbb R^d (k\le d)$ is discrete?
I know this is equivalent to saying that there is a ball centered at $O$ that only intersect the origin of the lattice.
To prove this statement, it suffices to prove that any ball only contains finitely many points in the lattice. This statement looks intuitively so obvious to me but I could never write down a formal proof.
If unnecessary, please do not identify the lattice with $GL(d,\mathbb R)/GL(d,\mathbb R)$. The topology in the latter is more complicated to me. Please just try to use elementary linear algebra and topology to prove this.
The setup and desired condition are both invariant under change of coordinates (because $GL_n(\mathbb{R})$ acts by homeomorphisms) so up to a suitable change of coordinates we can assume that the $v_i$ are the first $k$ vectors of the standard basis $e_i$ of $\mathbb{R}^n$. Now it's really easy: the lattice they span is a sublattice of $\mathbb{Z}^n$ so every point is at least a distance $1$ from every other point, so we can consider balls of radius $\frac{1}{2}$.
If that argument is distasteful to you we can rephrase it as follows: complete the $v_i$ to a basis of $\mathbb{R}^n$ and consider the inner product making the $v_i$ an orthonormal basis; then as above every lattice point is a distance of at least $1$ from every other in the norm induced by this inner product, and now we can appeal to the fact that every norm on $\mathbb{R}^n$ induces the Euclidean topology.
Alternatively, we can show that every ball contains at most finitely many lattice points by completing the lattice to a full rank lattice, then showing that every ball contains at most finitely many translates of a fundamental parallelepiped of this completed lattice. This follows because balls have finite volume and the fundamental parallelepiped has positive volume.