ascPochhammer_eval_succ — Mathlib

English

For any semiring S and natural r,n, the natural-cast version of the recurrence holds: the left-hand side with n as an element of S equals the right-hand side with n+r as an element of S.

Русский

Пусть S — полускольное кольцо, и n, r — натуральные числа. Неявная схема перехода сохраняется при переводе на кольцо S: левый и правый выражения совпадают после отображения по кольцу.

LaTeX

$$$ (n : S)\cdot (\operatorname{ascPochhammer} S\; r).eval(n+1 : S) = (n + r) \cdot (\operatorname{ascPochhammer} S\; r).eval(n : S) $$$

Lean4

theorem ascPochhammer_eval_succ (r n : ℕ) :
    (n : S) * (ascPochhammer S r).eval (n + 1 : S) = (n + r) * (ascPochhammer S r).eval (n : S) :=
  mod_cast congr_arg Nat.cast (ascPochhammer_nat_eval_succ r n)

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