English
Let f: σ → MvPolynomial τ R and g: τ → R. For p ∈ MvPolynomial σ R we have eval (eval g ∘ f) p = eval g (eval₂ C f p).
Русский
Пусть f: σ → MvPolynomial τ R и g: τ → R. Тогда eval (eval g ∘ f) p = eval g (eval₂ C f p).
LaTeX
$$$$\operatorname{eval}
(\operatorname{Function.comp}(\operatorname{eval} g)\, f)
(p) = \operatorname{eval}_g(\operatorname{eval}_2 \mathbf{C} f \, p).$$$$
Lean4
theorem eval_assoc {τ} (f : σ → MvPolynomial τ R) (g : τ → R) (p : MvPolynomial σ R) :
eval (eval g ∘ f) p = eval g (eval₂ C f p) :=
by
rw [eval₂_comp_left (eval g)]
unfold eval; simp only [coe_eval₂Hom]
congr with a; simp