English
Let StirlingFirst(n,k) be the (unsigned) Stirling number of the first kind: the number of permutations of n elements with exactly k disjoint cycles. It is defined by the recurrence: StirlingFirst(0,0)=1, StirlingFirst(0,k+1)=0, StirlingFirst(n+1,0)=0, StirlingFirst(n+1,k+1)=n·StirlingFirst(n,k+1)+StirlingFirst(n,k).
Русский
Пусть StirlingFirst(n,k) — неотрицательное число Стирлинга первого рода: число перестановок из n элементов, имеющих ровно k непересекающихся циклов. Рекуррентная формула: StirlingFirst(0,0)=1, StirlingFirst(0,k+1)=0, StirlingFirst(n+1,0)=0, StirlingFirst(n+1,k+1)=n·StirlingFirst(n,k+1)+StirlingFirst(n,k).
LaTeX
$$$\operatorname{stirlingFirst} : \mathbb{N} \times \mathbb{N} \to \mathbb{N}$ с заданной левой частью: \; \operatorname{stirlingFirst}(0,0)=1,\; \operatorname{stirlingFirst}(0,k+1)=0,\; \operatorname{stirlingFirst}(n+1,0)=0,\; \operatorname{stirlingFirst}(n+1,k+1)=n\cdot\operatorname{stirlingFirst}(n,k+1)+\operatorname{stirlingFirst}(n,k).$$$
Lean4
/-- `Nat.stirlingFirst n k` is the (unsigned) Stirling number of the first kind,
counting the number of permutations of `n` elements with exactly `k` disjoint cycles.
-/
def stirlingFirst : ℕ → ℕ → ℕ
| 0, 0 => 1
| 0, _ + 1 => 0
| _ + 1, 0 => 0
| n + 1, k + 1 => n * stirlingFirst n (k + 1) + stirlingFirst n k
