multichoose_eq — Mathlib

English

multichoose n k equals (n+k-1).choose k for all n,k.

Русский

multichoose n k равно (n+k-1).choose k для всех n,k.

LaTeX

$$$$ \operatorname{multichoose}(n,k) = \binom{n+k-1}{k} $$$$

Lean4

theorem multichoose_eq : ∀ n k : ℕ, multichoose n k = (n + k - 1).choose k
  | _, 0 => by simp
  | 0, k + 1 => by simp
  | n + 1, k + 1 =>
    by
    have : n + (k + 1) < (n + 1) + (k + 1) := Nat.add_lt_add_right (Nat.lt_succ_self _) _
    have : (n + 1) + k < (n + 1) + (k + 1) := Nat.add_lt_add_left (Nat.lt_succ_self _) _
    rw [multichoose_succ_succ, Nat.add_comm, Nat.succ_add_sub_one, ← Nat.add_assoc, Nat.choose_succ_succ]
    simp [multichoose_eq n (k + 1), multichoose_eq (n + 1) k]

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