descFactorial_eq_div — Mathlib

English

If k ≤ n, then the descending factorial equals n! divided by (n−k)!; i.e. n.descFactorial k = n! / (n−k)!.

Русский

Если k ≤ n, то n↓k = n!/(n−k)!.

LaTeX

$$n.descFactorial k = n! / (n - k)! \\\\ (k ≤ n)$$

Lean4

/-- Avoid in favor of `Nat.factorial_mul_descFactorial` if you can. ℕ-division isn't worth it. -/
theorem descFactorial_eq_div {n k : ℕ} (h : k ≤ n) : n.descFactorial k = n ! / (n - k)! :=
  by
  apply Nat.mul_left_cancel (n - k).factorial_pos
  rw [factorial_mul_descFactorial h]
  exact (Nat.mul_div_cancel' <| factorial_dvd_factorial <| Nat.sub_le n k).symm

Похожие утверждения