factorial_mul_ascPochhammer — Mathlib

English

For natural numbers n and m, ascPochhammer S n · (ascPochhammer S m).comp (X + n) = ascPochhammer S (n+m).

Русский

Для натуральных n,m: ascPochhammer S n · (ascPochhammer S m).comp (X + n) = ascPochhammer S (n+m).

LaTeX

$$$ascPochhammer S n * (ascPochhammer S m).\\mathrm{comp}(X + n) = ascPochhammer S (n+m)$$$

Lean4

theorem factorial_mul_ascPochhammer (S : Type*) [Semiring S] (r n : ℕ) :
    (r ! : S) * (ascPochhammer S n).eval (r + 1 : S) = (r + n)! := by
  rw_mod_cast [ascPochhammer_nat_eq_ascFactorial, Nat.factorial_mul_ascFactorial]

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