ascFactorial_eq_div — Mathlib

English

For all n,k ∈ ℕ, (n+1)^{\overline{k}} = (n+k)! / n!.

Русский

Для всех n,k ∈ ℕ: (n+1)^{\overline{k}} = (n+k)! / n!.

LaTeX

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

Lean4

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

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