English
For anyNatPowAssoc ring R, the binomial coefficient evaluated at n cast to R equals the natural binomial coefficient of n cast as a natural number: choose (n : R) k = (Nat.choose n k).cast.
Русский
Для кольца R с NatPowAssoc выполняется равенство choose (n : R) k = (Nat.choose n k).cast.
LaTeX
$$$ \forall R\ [NatPowAssoc\ R]\ (n,k:\mathbb{N}),\ choose\ (n:\,R)\ k = (\mathrm{Nat}.\choose\ n\ k)\;\text{cast}$$$
Lean4
theorem choose_natCast [NatPowAssoc R] (n k : ℕ) : choose (n : R) k = Nat.choose n k := by
rw [← nsmul_right_inj (Nat.factorial_ne_zero k), ← descPochhammer_eq_factorial_smul_choose, nsmul_eq_mul, ←
Nat.cast_mul, ← Nat.descFactorial_eq_factorial_mul_choose, ← descPochhammer_smeval_eq_descFactorial]
