English
Let R and S be commutative semirings and let p be a polynomial in finitely many variables indexed by σ with coefficients in R. If k: σ → τ and g: τ → S, then evaluating the renamed polynomial at g is the same as renaming with k first and then evaluating via g, i.e. aeval g (rename k p) = aeval (g ∘ k) p.
Русский
Пусть R и S — коммутативные полугруппы без нулей, а p — многочлен от переменных, индексируемых σ, с коэффициентами в R. Пусть k: σ → τ и g: τ → S. Тогда после переименования p по k и применения aeval g получим то же, что и если сначала переименовать p по k и затем применить aeval к g ∘ k: aeval g (rename k p) = aeval (g ∘ k) p.
LaTeX
$$$ (\mathrm{aeval}\ g)\,(\mathrm{rename}\ k\ p) = (\mathrm{aeval}\ (g \circ k))\ p $$$
Lean4
theorem aeval_rename [Algebra R S] : aeval g (rename k p) = aeval (g ∘ k) p :=
eval₂Hom_rename _ _ _ _
