Commit 2026-02-16 21:07 32fe3f93

feat: the left uniformity in a group (#35252) We have currently a specific definition of the right uniformity of a topological group, but not of the left uniformity. We introduce it in the current PR, for two reasons. First, there is no reason to favor one over the other. Second, it is needed in #35037, which changes the formula for the distance in a normed group to make it left-invariant following standard conventions. We also prove that a group is complete for its left-uniformity iff it is complete for its right-uniformity, by showing that inversion is a uniform equivalence between the two uniformities.