English
Let R be a (nonassociative) semiring with a compatible N-power structure and a binomial ring structure. For every natural k and every n ∈ ℕ, evaluating the ascending Pochhammer polynomial with natural coefficients at n, after casting n into R, yields the same result as evaluating at n in ℕ and then casting the result to R. In other words, smeval (ascPochhammer ℕ k) evaluated at (n : R) equals smeval (ascPochhammer ℕ k) n.
Русский
Пусть R — полукольцо (в частности, неассоциативное) с совместимой структурой возведения в натуральную степень и биномиальным кольцом. Для любого натурального k и любого n ∈ ℕ применение функции smeval к многочлену ascPochhammer ℕ k к элементу n, затем приведённому к R, даёт тот же результат, что и применение smeval к ascPochhammer ℕ k к числу n в ℕ, затем переход к R. То есть smeval (ascPochhammer ℕ k) (n : R) = smeval (ascPochhammer ℕ k) n.
LaTeX
$$$ \forall R\ [NonAssocSemiring\ R]\ [Pow\ R\ \mathbb{N}]\ [NatPowAssoc\ R],\ (n,k)\in\mathbb{N} :\quad \mathrm{smeval}\big(\ascPochhammer\ \mathbb{N}\ k\big)\big(n:\,R\big) = \mathrm{smeval}\big(\ascPochhammer\ \mathbb{N}\ k\big)\,n$$$
Lean4
theorem smeval_ascPochhammer_nat_cast {R} [NonAssocSemiring R] [Pow R ℕ] [NatPowAssoc R] (n k : ℕ) :
smeval (ascPochhammer ℕ k) (n : R) = smeval (ascPochhammer ℕ k) n := by rw [smeval_at_natCast (ascPochhammer ℕ k) n]
