 Birkhoff-Kakutani theorem

A Hausdorff topological group admits a compatible left-invariant group metric exactly when it has a countable neighbourhood basis at the identity element. Choose symmetric neighbourhoods of the identity element $U_n$ with $U_{n+1}^3\subset U_n$ and trivial intersection. Assign a step in $U_n$ cost $2^{-n}$, and take the infimum of total costs of chains joining two points. The dyadic product estimate for group neighbourhoods makes this a genuine compatible metric. The Hausdorff assumption separates distinct points; without it the same construction can give only a pseudometric.