Cast of binomial coefficients #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file allows calculating the binomial coefficient a.choose b
as an element of a division ring
of characteristic 0
.
theorem
nat.cast_choose_eq_pochhammer_div
(K : Type u_1)
[division_ring K]
[char_zero K]
(a b : ℕ) :