We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent d9de1d9 commit c6e2cb8Copy full SHA for c6e2cb8
1 file changed
Mathlib/Combinatorics/Enumerative/Stirling.lean
@@ -52,7 +52,7 @@ def stirlingFirst : ℕ → ℕ → ℕ
52
| n + 1, k + 1 => n * stirlingFirst n (k + 1) + stirlingFirst n k
53
54
@[simp]
55
-theorem stirlingFirst_zero: stirlingFirst 0 0 = 1 :=
+theorem stirlingFirst_zero : stirlingFirst 0 0 = 1 :=
56
rfl
57
58
0 commit comments