English
Under suitable unitness of m!, the cast of a binomial coefficient equals m! times the inverses of k! and (m−k)!, when k ∈ antidiagonal m.
Русский
При подходящей единичности m! надень Cast биномиального коэффициента равен m! умножить на обратные k! и (m−k)!, когда k принадлежит антидиагонали m.
LaTeX
$$$ \uparrow( {m \choose k} ) = m! \cdot (k!)^{-1} \cdot ((m-k)!)^{-1} $ (при условии, что m! является единицей)$$
Lean4
theorem castChoose_eq {A : Type*} [CommSemiring A] {m : ℕ} {k : ℕ × ℕ} (hm : IsUnit (m ! : A))
(hk : k ∈ Finset.antidiagonal m) : (choose m k.1 : A) = ↑m ! * inverse ↑k.1! * inverse ↑k.2! :=
by
rw [Finset.mem_antidiagonal] at hk
subst hk
rw [eq_mul_inverse_iff_mul_eq, eq_mul_inverse_iff_mul_eq, ← Nat.cast_mul, ← Nat.cast_mul, add_comm,
Nat.add_choose_mul_factorial_mul_factorial] <;>
apply hm.natCast_factorial_of_le
exacts [Nat.le_add_right k.1 k.2, Nat.le_add_left k.2 k.1]
