Small clarification on multiple renamings

interacting_with_lean.rst

@@ -250,7 +250,7 @@ creates aliases for everything in the ``nat`` namespace *except* the identifiers
     open nat (renaming mul → times) (renaming add → plus)
       (hiding succ sub)
 
-creates aliases for everything in the ``nat`` namespace except ``succ`` and ``sub``, renaming ``nat.add`` to ``plus``.
+creates aliases for everything in the ``nat`` namespace except ``succ`` and ``sub``, renaming ``nat.mul`` to ``times` and ``nat.add`` to ``plus``.
 
 It is sometimes useful to ``export`` aliases from one namespace to another, or to the top level. The command