choose_add_smul_choose — Mathlib

English

A form of Chu-Vandermonde: (n+k choose k)•choose (r+k) (n+k) = choose (r+k) k · choose r n.

Русский

Форма Чу-Вандермонда: (n+k выбрать k) • choose (r+k) (n+k) = choose (r+k) k · choose r n.

LaTeX

$$$ \forall R\ [NonAssocRing\ R]\ [Pow\ R\ Nat]\ [BinomialRing\ R]\ (r: R)\ {n k : \mathbb{N}},\ (\binom{n+k}{k})\cdot \mathrm{choose}(r+k)(n+k) = \mathrm{choose}(r+k)k \cdot \mathrm{choose} r n$$$

Lean4

theorem choose_add_smul_choose [NatPowAssoc R] (r : R) (n k : ℕ) :
    (Nat.choose (n + k) k) • choose (r + k) (n + k) = choose (r + k) k * choose r n := by
  rw [choose_smul_choose (r + k) (Nat.le_add_left k n), Nat.add_sub_cancel, add_sub_cancel_right]

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