ascFactorial_eq_div' — Mathlib

English

If n > 0, n.ascFactorial k = (n + k - 1)! / (n - 1)!.

Русский

Если n > 0, то n^{\overline{k}} = (n+k-1)! / (n-1)!.

LaTeX

$$$$\forall n,k \in \mathbb{N}, n>0 \Rightarrow n^{\overline{k}} = \frac{(n+k-1)!}{(n-1)!}$$$$

Lean4

/-- Avoid in favor of `Nat.factorial_mul_ascFactorial'` if you can. ℕ-division isn't worth it. -/
theorem ascFactorial_eq_div' (n k : ℕ) (h : 0 < n) : n.ascFactorial k = (n + k - 1)! / (n - 1)! :=
  Nat.eq_div_of_mul_eq_right (n - 1).factorial_ne_zero (factorial_mul_ascFactorial' _ _ h)

Похожие утверждения