 Left-invariant group metric

This is a distance function satisfying the displayed identity, rather than a Riemannian metric tensor. When it induces the group's given topology, it is a compatible left-invariant group metric. Left translations are isometries.