English
For a commutative semiring R, a polynomial p over R, and an algebra S over R, the evaluation of the composed ascPochhammer equals the nested evaluation: ((ascPochhammer S n).comp (p.map (algebraMap R S))).eval x = (ascPochhammer S n).eval (p.eval₂ (algebraMap R S) x).
Русский
Для коммутативного полугрего R и алгебра над R, значение сложенного ascPochhammer равно вложенной оценке: ... = ...
LaTeX
$$$((ascPochhammer\\, S\\, n).\\mathrm{comp}(p\\mapsto (\\mathrm{algebraMap}\\, R\\, S)))\\mathrm{eval}\\ x = (ascPochhammer\\, S\\, n).\\mathrm{eval}(p.\\mathrm{eval_2}(\\mathrm{algebraMap}\\, R\\, S)\\ x)$$$
Lean4
theorem ascPochhammer_eval_comp {R : Type*} [CommSemiring R] (n : ℕ) (p : R[X]) [Algebra R S] (x : S) :
((ascPochhammer S n).comp (p.map (algebraMap R S))).eval x =
(ascPochhammer S n).eval (p.eval₂ (algebraMap R S) x) :=
by
rw [ascPochhammer_eval₂ (algebraMap R S), ← eval₂_comp', ← ascPochhammer_map (algebraMap R S), ← map_comp, eval_map]
