We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 616fb9b commit e37d360Copy full SHA for e37d360
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