Commit 2024-11-16 15:42 b4ef1175

chore: don't use TopologicalGroup.toUniformSpace in tendstoUniformly_iff (#19098) This changes TopologicalGroup.tendstoUniformly_iff so that it takes a UniformSpace instance instead of only a TopologicalGroup instance, along with a proof that the uniform space is the one induced by the topological group structure. The previous version would have been hard to use in case you had, for example, a normed commutative group, as the uniform space structure inferred would not match (defeq) the one given in this theorem, which was previously TopologicalSpace.toUniformSpace.