descFactorial — Mathlib

English

descFactorial(n,k) = n! / (n-k)!.

Русский

descFactorial(n,k) = n! / (n-k)!.

LaTeX

$$$$\operatorname{descFactorial}(n,k) = \frac{n!}{(n-k)!}$$$$

Lean4

/-- `n.descFactorial k = n! / (n - k)!` (as seen in `Nat.descFactorial_eq_div`), but
implemented recursively to allow for "quick" computation when using `norm_num`. This is closely
related to `descPochhammer`, but much less general. -/
def descFactorial (n : ℕ) : ℕ → ℕ
  | 0 => 1
  | k + 1 => (n - k) * descFactorial n k

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