ascFactorial — Mathlib

English

Definition: ascFactorial(n,k) = n(n+1)⋯(n+k−1), with ascFactorial(n,0) = 1.

Русский

Определение: ascFactorial(n,k) = n(n+1)⋯(n+k−1), при этом ascFactorial(n,0) = 1.

LaTeX

$$$\mathrm{ascFactorial}(n,k) = \prod_{i=0}^{k-1} (n+i)$$$

Lean4

/-- `n.ascFactorial k = n (n + 1) ⋯ (n + k - 1)`. This is closely related to `ascPochhammer`, but
much less general. -/
def ascFactorial (n : ℕ) : ℕ → ℕ
  | 0 => 1
  | k + 1 => (n + k) * ascFactorial n k

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