prod_range_add_one_eq_factorial — Mathlib

English

For any α and endomorphism structure S, a! equals the evaluation of the rising factorial (ascPochhammer S b) at a cast of a, connecting with ascending factorial identities.

Русский

Для любой структуры S и чисел a,b связь между факториалом и восходящим pochhammer: a! = (ascPochhammer S b).eval (a).

LaTeX

$$a! = (ascPochhammer S b).eval (a)$$

Lean4

@[simp]
theorem _root_.Finset.prod_range_add_one_eq_factorial (n : ℕ) : ∏ i ∈ range n, (i + 1) = (n)! :=
  factorial_eq_prod_range_add_one _ |>.symm

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