descPochhammer_succ_left — Mathlib

English

For any ring R and natural n, the successor satisfies: descPochhammer R (n+1) = X · (descPochhammer R n) ◦ (X−1).

Русский

Для кольца R и натурального n выполнено: descendPochhammer R (n+1) = X · (descPochhammer R n) ◦ (X−1).

LaTeX

$$$\operatorname{descPochhammer}_R(n+1) = X \cdot (\operatorname{descPochhammer}_R(n)) \circ (X-1)$$$

Lean4

theorem descPochhammer_succ_left (n : ℕ) : descPochhammer R (n + 1) = X * (descPochhammer R n).comp (X - 1) := by
  rw [descPochhammer]

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