mathlib3

fa41b7aa - feat(topology/algebra/uniform_group): Condition for uniform convergence (#11391)

feat(topology/algebra/uniform_group): Condition for uniform convergence (#11391) This PR adds a lemma regarding uniform convergence on a topological group `G`, placed right after the construction of the `uniform_space` structure on `G`.