lint(topology/algebra): docstrings (#4446)

Co-authored-by: hrmacbeth <25316162+hrmacbeth@users.noreply.github.com>

src/topology/algebra/group.lean

@@ -86,7 +86,8 @@ instance [topological_group α] [topological_space β] [group β] [topological_g
 
 attribute [instance] prod.topological_add_group
 
-@[to_additive]
+/-- Multiplication from the left in a topological group as a homeomorphism.-/
+@[to_additive "Addition from the left in a topological additive group as a homeomorphism."]
 protected def homeomorph.mul_left [topological_group α] (a : α) : α ≃ₜ α :=
 { continuous_to_fun  := continuous_const.mul continuous_id,
   continuous_inv_fun := continuous_const.mul continuous_id,
@@ -100,7 +101,8 @@ lemma is_open_map_mul_left [topological_group α] (a : α) : is_open_map (λ x,
 lemma is_closed_map_mul_left [topological_group α] (a : α) : is_closed_map (λ x, a * x) :=
 (homeomorph.mul_left a).is_closed_map
 
-@[to_additive]
+/-- Multiplication from the right in a topological group as a homeomorphism.-/
+@[to_additive "Addition from the right in a topological additive group as a homeomorphism."]
 protected def homeomorph.mul_right
   {α : Type*} [topological_space α] [group α] [topological_group α] (a : α) :
   α ≃ₜ α :=
@@ -116,7 +118,8 @@ lemma is_open_map_mul_right [topological_group α] (a : α) : is_open_map (λ x,
 lemma is_closed_map_mul_right [topological_group α] (a : α) : is_closed_map (λ x, x * a) :=
 (homeomorph.mul_right a).is_closed_map
 
-@[to_additive]
+/-- Inversion in a topological group as a homeomorphism.-/
+@[to_additive "Negation in a topological group as a homeomorphism."]
 protected def homeomorph.inv (α : Type*) [topological_space α] [group α] [topological_group α] :
   α ≃ₜ α :=
 { continuous_to_fun  := continuous_inv,

src/topology/algebra/open_subgroup.lean

@@ -107,7 +107,8 @@ end
 section
 variables {H : Type*} [group H] [topological_space H]
 
-@[to_additive]
+/-- The product of two open subgroups as an open subgroup of the product group. -/
+@[to_additive "The product of two open subgroups as an open subgroup of the product group."]
 def prod (U : open_subgroup G) (V : open_subgroup H) : open_subgroup (G × H) :=
 { carrier := (U : set G).prod (V : set H),
   is_open' := is_open_prod U.is_open V.is_open,

src/topology/algebra/ring.lean

@@ -47,6 +47,7 @@ end topological_ring
 section topological_comm_ring
 variables {α : Type*} [topological_space α] [comm_ring α] [topological_ring α]
 
+/-- The closure of an ideal in a topological ring as an ideal. -/
 def ideal.closure (S : ideal α) : ideal α :=
 { carrier := closure S,
   zero_mem' := subset_closure S.zero_mem,

src/topology/algebra/uniform_group.lean

@@ -145,6 +145,7 @@ open filter
 variables {G : Type u} [add_comm_group G] [topological_space G] [topological_add_group G]
 
 variable (G)
+/-- The right uniformity on a topological group. -/
 def topological_add_group.to_uniform_space : uniform_space G :=
 { uniformity          := comap (λp:G×G, p.2 - p.1) (𝓝 0),
   refl                :=
@@ -228,6 +229,7 @@ variables [add_comm_group α] [add_comm_group β] [add_comm_group γ]
 
 /- TODO: when modules are changed to have more explicit base ring, then change replace `is_Z_bilin`
 by using `is_bilinear_map ℤ` from `tensor_product`. -/
+/-- `ℤ`-bilinearity for maps between additive commutative groups. -/
 class is_Z_bilin (f : α × β → γ) : Prop :=
 (add_left []  : ∀ a a' b, f (a + a', b) = f (a, b) + f (a', b))
 (add_right [] : ∀ a b b', f (a, b + b') = f (a, b) + f (a, b'))

src/topology/algebra/uniform_ring.lean

@@ -149,6 +149,9 @@ lemma ring_sep_quot (α) [r : comm_ring α] [uniform_space α] [uniform_add_grou
   quotient (separation_setoid α) = (⊥ : ideal α).closure.quotient :=
 by rw [@ring_sep_rel α r]; refl
 
+/-- Given a topological ring `α` equipped with a uniform structure that makes subtraction uniformly
+continuous, get an equivalence between the separated quotient of `α` and the quotient ring
+corresponding to the closure of zero. -/
 def sep_quot_equiv_ring_quot (α)
   [r : comm_ring α] [uniform_space α] [uniform_add_group α] [topological_ring α] :
   quotient (separation_setoid α) ≃ (⊥ : ideal α).closure.quotient :=