Discrete subgroups are closed embedded zero-dimensional Lie subgroups

Suppose $\mathrm{\Gamma }$ is discrete in the subspace topology. There is an identity neighborhood $U$ with $U\cap \mathrm{\Gamma }=\{e\}$. Choose a symmetric identity neighborhood $V$ with $V^{-1}V\subseteq U$. Every translate $gV$ contains at most one point of $\mathrm{\Gamma }$: two such points ${\gamma }_1,{\gamma }_2$ would satisfy ${\gamma }_1^{-1}{\gamma }_2\in U\cap \mathrm{\Gamma }$.

If $g$ lies in the closure of $\mathrm{\Gamma }$, then $gV$ contains some $\gamma \in \mathrm{\Gamma }$. If $g\mathrm{\ne }\gamma$, Hausdorffness makes $(gV)\setminus \{\gamma \}$ an open neighborhood of $g$ disjoint from $\mathrm{\Gamma }$, contradicting closure. Thus $g=\gamma$, so $\mathrm{\Gamma }$ is closed.

By [A1], $\mathrm{\Gamma }$ has its unique embedded Lie-subgroup structure. Its embedded topology is its discrete subspace topology, so every singleton is an open coordinate neighborhood; hence its manifold dimension is zero.

Conversely, an embedded zero-dimensional Lie subgroup has the subspace topology, and every point has a chart into the one-point space ${\mathbb{R}}^0$; it is therefore discrete. Its closedness is already part of the right-hand condition. This proves both directions. The trivial subgroup and discrete ambient groups are included. Choice is used only through [A1].