English
For any r and naturals n,k with n≥k, (n choose k)·choose r n = choose r k · choose (r−k) (n−k).
Русский
Для любых r и нa натуральных n,k с n≥k выполняется (n choose k)·choose r n = choose r k · choose (r−k) (n−k).
LaTeX
$$$ \forall R\ [NonAssocRing\ R]\ [Pow\ R\ Nat]\ [BinomialRing\ R]\ (r: R)\ {n k : \mathbb{N}},\ (n \choose k) \cdot choose r n = choose r k \cdot choose (r - k) (n - k)$$$
Lean4
theorem choose_smul_choose [NatPowAssoc R] (r : R) {n k : ℕ} (hkn : k ≤ n) :
(Nat.choose n k) • choose r n = choose r k * choose (r - k) (n - k) :=
by
rw [← nsmul_right_inj (Nat.factorial_ne_zero n), nsmul_left_comm, ← descPochhammer_eq_factorial_smul_choose, ←
Nat.choose_mul_factorial_mul_factorial hkn, ← smul_mul_smul_comm, ← descPochhammer_eq_factorial_smul_choose,
mul_nsmul', ← descPochhammer_eq_factorial_smul_choose, smul_mul_assoc]
nth_rw 2 [← Nat.sub_add_cancel hkn]
rw [add_comm, ← descPochhammer_mul, smeval_mul, smeval_comp, smeval_sub, smeval_X, ← C_eq_natCast, smeval_C, npow_one,
npow_zero, zsmul_one, Int.cast_natCast, nsmul_eq_mul]
