Binomial coefficients and inverse factorials

The factorial quotient formula for a binomial coefficient gives identities between products of inverse factorials in a characteristic-zero division semiring. These are the scalar identities used in the multiplication and binomial formulas for divided powers.

theorem Nat.inv_factorial_mul_inv_factorial {K : Type u_1} [DivisionSemiring K] [CharZero K] (m n : ℕ) : (↑m.factorial)⁻¹ * (↑n.factorial)⁻¹ = ↑((m + n).choose m) * (↑(m + n).factorial)⁻¹

A product of inverse factorials is the binomial coefficient times the inverse factorial of the sum.

theorem Nat.inv_factorial_mul_choose {K : Type u_1} [DivisionSemiring K] [CharZero K] (n i j : ℕ) (hij : i + j = n) : (↑n.factorial)⁻¹ * ↑(n.choose i) = (↑i.factorial)⁻¹ * (↑j.factorial)⁻¹

Multiplying an inverse factorial by a binomial coefficient splits it into the inverse factorials of the two complementary indices.