diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el
index cd99a083d8..61603004b8 100644
--- a/src/emacs/lean-syntax.el
+++ b/src/emacs/lean-syntax.el
@@ -130,7 +130,7 @@
       (1 'font-lock-doc-face))
      (,(rx (group "#" (or "eval" "print" "reduce" "help" "check")))
       (1 'font-lock-keyword-face))
-     ;; mutal definitions "names"
+     ;; mutual definitions "names"
      (,(rx word-start
            "mutual"
            word-end
diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp
index d9764c3457..be8608e79d 100644
--- a/src/frontends/lean/decl_cmds.cpp
+++ b/src/frontends/lean/decl_cmds.cpp
@@ -559,7 +559,7 @@ void register_decl_cmds(cmd_table & r) {
     add_cmd(r, cmd_info("constants",       "declare new constants (aka top-level variables)", constants_cmd));
     add_cmd(r, cmd_info("axioms",          "declare new axioms", axioms_cmd));
     add_cmd(r, cmd_info("meta",            "add new meta declaration", modifiers_cmd, false));
-    add_cmd(r, cmd_info("mutual",          "add new mutal declaration", modifiers_cmd, false));
+    add_cmd(r, cmd_info("mutual",          "add new mutual declaration", modifiers_cmd, false));
     add_cmd(r, cmd_info("noncomputable",   "add new noncomputable definition", modifiers_cmd, false));
     add_cmd(r, cmd_info("private",         "add new private declaration", modifiers_cmd, false));
     add_cmd(r, cmd_info("protected",       "add new protected declaration", modifiers_cmd, false));