succ_mul_choose_eq — Mathlib

English

For all n,k: (n+1) * C(n,k) = (k+1) * C(n+1, k+1).

Русский

Для любых n,k: (n+1) \\, C(n,k) = (k+1) \\, C(n+1, k+1).

LaTeX

$$$\\\\binom{n}{k} (k+1) = \\\\binom{n+1}{k+1} (k+1)$$$

Lean4

theorem succ_mul_choose_eq : ∀ n k, succ n * choose n k = choose (succ n) (succ k) * succ k
  | 0, 0 => by decide
  | 0, k + 1 => by simp [choose]
  | n + 1, 0 => by simp [choose, mul_succ, Nat.add_comm]
  | n + 1, k + 1 => by
    rw [choose_succ_succ (succ n) (succ k), Nat.add_mul, ← succ_mul_choose_eq n, mul_succ, ← succ_mul_choose_eq n,
      Nat.add_right_comm, ← Nat.mul_add, ← choose_succ_succ, ← succ_mul]

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