descPochhammer_int_eq_ascFactorial

English

For natural a,b, the evaluation of (descPochhammer ℤ b) at a+b equals the ascFactorial a+1 evaluated at b.

Русский

Для натуральных a,b: (descPochhammer ℤ b).eval (a+b) = (a+1).ascFactorial b.

LaTeX

$$$(\operatorname{descPochhammer}_{\mathbb{Z}} b).eval(a+b) = (a+1).\ascFactorial b$$$

Lean4

theorem descPochhammer_int_eq_ascFactorial (a b : ℕ) : (descPochhammer ℤ b).eval (a + b : ℤ) = (a + 1).ascFactorial b :=
  by rw [← Nat.cast_add, descPochhammer_eval_eq_descFactorial ℤ (a + b) b, Nat.add_descFactorial_eq_ascFactorial]

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