docs(topology/basic): Fix typo in library note (#14743)

leanprover-community · Jun 15, 2022 · 784c703 · 784c703
1 parent 1fbe118
commit 784c703
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/topology/basic.lean b/src/topology/basic.lean
@@ -1556,7 +1556,7 @@ However, lemmas with this conclusion are not nice to use in practice because
 1. They confuse the elaborator. The following two examples fail, because of limitations in the
   elaboration process.
   ```
-  variables {M : Type*} [has_mul M] [topological_space M] [has_continuous_mul M]
+  variables {M : Type*} [has_add M] [topological_space M] [has_continuous_add M]
   example : continuous (λ x : M, x + x) :=
   continuous_add.comp _