English
Let n and k be natural numbers. The falling factorial of n+k−1 with length k equals the rising factorial of n with length k; i.e. (n+k−1)↓k = n↑k, which concretely is (n+k−1)(n+k−2)⋯n = n(n+1)⋯(n+k−1).
Русский
Пусть n и k — натуральные числа. Нисходящий факториал (n+k−1) на длину k равен восходящему факториалу n на длину k; тождество (n+k−1)↓k = n↑k, то есть (n+k−1)(n+k−2)⋯n = n(n+1)⋯(n+k−1).
LaTeX
$$$(n+k-1)^{\\downarrow k} = n^{\\uparrow k}$$$
Lean4
theorem add_descFactorial_eq_ascFactorial' (n : ℕ) : ∀ k : ℕ, (n + k - 1).descFactorial k = n.ascFactorial k
| 0 => by rw [ascFactorial_zero, descFactorial_zero]
| succ k => by
rw [descFactorial_succ, ascFactorial_succ, ← succ_add_eq_add_succ, add_descFactorial_eq_ascFactorial' _ k, ←
succ_ascFactorial, succ_add_sub_one, Nat.add_sub_cancel]
