ascPochhammer_smeval_eq_eval — Mathlib

English

For any semiring R, smeval of ascPochhammer ℕ n equals eval of ascPochhammer R n at the same input; i.e., the two ways of interpreting the polynomial coincide.

Русский

Для любого полупрямоугольного кольца R, smeval ascPochhammer ℕ n совпадает с eval ascPochhammer R n.

LaTeX

$$$\text{(ascPochhammer} \mathbb{N} \; n).\mathrm{smeval}\; x = \text{(ascPochhammer} R \; n).\mathrm{eval}\; x$$$

Lean4

theorem ascPochhammer_smeval_eq_eval [Semiring R] (r : R) (n : ℕ) :
    (ascPochhammer ℕ n).smeval r = (ascPochhammer R n).eval r := by rw [eval_eq_smeval, ascPochhammer_smeval_cast R]

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