factorial_mul_ascFactorial — Mathlib

English

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

Русский

Для всех n,k ∈ ℕ выполняется: n! · (n+1)^{\overline{k}} = (n+k)!.

LaTeX

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

Lean4

/-- `(n + 1).ascFactorial k = (n + k) ! / n !` but without ℕ-division. See
`Nat.ascFactorial_eq_div` for the version with ℕ-division. -/
theorem factorial_mul_ascFactorial (n : ℕ) : ∀ k, n ! * (n + 1).ascFactorial k = (n + k)!
  | 0 => by rw [ascFactorial_zero, Nat.add_zero, Nat.mul_one]
  | k + 1 => by
    rw [ascFactorial_succ, ← Nat.add_assoc, factorial_succ, Nat.mul_comm (n + 1 + k), ← Nat.mul_assoc,
      factorial_mul_ascFactorial n k, Nat.mul_comm, Nat.add_right_comm]

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