fix(data/nat/factorial): fix factorial_zero (#7697)

leanprover-community · May 23, 2021 · 2734d91 · 2734d91
1 parent 6cffc9f
commit 2734d91
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/data/nat/factorial.lean b/src/data/nat/factorial.lean
@@ -22,7 +22,7 @@ section factorial
 
 variables {m n : ℕ}
 
-@[simp] theorem factorial_zero : 0! = 1! := rfl
+@[simp] theorem factorial_zero : 0! = 1 := rfl
 
 @[simp] theorem factorial_succ (n : ℕ) : n.succ! = succ n * n! := rfl