ascFactorial_eq_factorial_mul_choose

English

For i,j ∈ ℕ, (i+j choose j) i! j! = (i+j)!.

Русский

Для любых i,j ∈ ℕ: (i+j choose j) i! j! = (i+j)!.

LaTeX

$$$\\\\binom{i+j}{j} \\\\cdot i! \\\\cdot j! = (i+j)!$$$

Lean4

theorem ascFactorial_eq_factorial_mul_choose (n k : ℕ) : (n + 1).ascFactorial k = k ! * (n + k).choose k :=
  by
  rw [Nat.mul_comm]
  apply Nat.mul_right_cancel (n + k - k).factorial_pos
  rw [choose_mul_factorial_mul_factorial <| Nat.le_add_left k n, Nat.add_sub_cancel_right, ← factorial_mul_ascFactorial,
    Nat.mul_comm]

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