From 21c48e1fee160fa2d3d83796b5620978c9f58f04 Mon Sep 17 00:00:00 2001
From: mcdoll <moritz.doll@googlemail.com>
Date: Tue, 5 Apr 2022 08:08:57 +0000
Subject: [PATCH] doc(topology/algebra/*): explanation of relation between
 `uniform_group` and `topological_group` (#13151)

Adding some comments on how to use `uniform_group` and `topological_group`.
---
 src/topology/algebra/group.lean         |  8 ++++++--
 src/topology/algebra/uniform_group.lean | 10 ++++++++++
 2 files changed, 16 insertions(+), 2 deletions(-)

diff --git a/src/topology/algebra/group.lean b/src/topology/algebra/group.lean
index 76d05e0ab8ffd..9d492f562f0d9 100644
--- a/src/topology/algebra/group.lean
+++ b/src/topology/algebra/group.lean
@@ -11,7 +11,7 @@ import topology.sets.compacts
 import topology.algebra.constructions
 
 /-!
-# Theory of topological groups
+# Topological groups
 
 This file defines the following typeclasses:
 
@@ -330,7 +330,11 @@ class topological_add_group (G : Type u) [topological_space G] [add_group G]
   extends has_continuous_add G, has_continuous_neg G : Prop
 
 /-- A topological group is a group in which the multiplication and inversion operations are
-continuous. -/
+continuous.
+
+When you declare an instance that does not already have a `uniform_space` instance,
+you should also provide an instance of `uniform_space` and `uniform_group` using
+`topological_group.to_uniform_space` and `topological_group_is_uniform`. -/
 @[to_additive]
 class topological_group (G : Type*) [topological_space G] [group G]
   extends has_continuous_mul G, has_continuous_inv G : Prop
diff --git a/src/topology/algebra/uniform_group.lean b/src/topology/algebra/uniform_group.lean
index 9156ee28e8e45..3a04961fa4a7e 100644
--- a/src/topology/algebra/uniform_group.lean
+++ b/src/topology/algebra/uniform_group.lean
@@ -12,6 +12,16 @@ import tactic.abel
 /-!
 # Uniform structure on topological groups
 
+This file defines uniform groups and its additive counterpart. These typeclasses should be
+preferred over using `[topological_space α] [topological_group α]` since every topological
+group naturally induces a uniform structure.
+
+## Main declarations
+* `uniform_group` and `uniform_add_group`: Multiplicative and additive uniform groups, that
+  i.e., groups with uniformly continuous `(*)` and `(⁻¹)` / `(+)` and `(-)`.
+
+## Main results
+
 * `topological_add_group.to_uniform_space` and `topological_add_group_is_uniform` can be used to
   construct a canonical uniformity for a topological add group.