ascPochhammer_succ_eval — Mathlib

English

For any n and k in a semiring S, (ascPochhammer S (n+1)).eval k = (ascPochhammer S n).eval k · (k + n).

Русский

Для любых n, k в полугруппе S: (ascPochhammer S (n+1)).eval k = (ascPochhammer S n).eval k · (k + n).

LaTeX

$$$(ascPochhammer S (n+1)).\\mathrm{eval} k = (ascPochhammer S n).\\mathrm{eval} k \\cdot (k + n)$$$

Lean4

theorem ascPochhammer_succ_eval {S : Type*} [Semiring S] (n : ℕ) (k : S) :
    (ascPochhammer S (n + 1)).eval k = (ascPochhammer S n).eval k * (k + n) := by
  rw [ascPochhammer_succ_right, mul_add, eval_add, eval_mul_X, ← Nat.cast_comm, ← C_eq_natCast, eval_C_mul,
    Nat.cast_comm, ← mul_add]

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