ascPochhammer_eval_one — Mathlib

English

A composition identity: (ascPochhammer S (n+1)).comp (X+1) = ascPochhammer S (n+1) + (n+1) • (ascPochhammer S n).comp (X+1).

Русский

Идентичность композиции: (ascPochhammer S (n+1)).comp (X+1) = ascPochhammer S (n+1) + (n+1) • (ascPochhammer S n).comp (X+1).

LaTeX

$$$(ascPochhammer S (n+1)).\\mathrm{comp}(X+1) = ascPochhammer S (n+1) + (n+1) \\cdot (ascPochhammer S n).\\mathrm{comp}(X+1)$$$

Lean4

@[simp]
theorem ascPochhammer_eval_one (S : Type*) [Semiring S] (n : ℕ) : (ascPochhammer S n).eval (1 : S) = (n ! : S) := by
  rw_mod_cast [ascPochhammer_nat_eq_ascFactorial, Nat.one_ascFactorial]

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