English
For a ring hom f: R →+* S and a family g: σ → MvPolynomial τ S, and p ∈ MvPolynomial σ R, evaluating eval₂ after eval₂ equals eval₂ with composed maps: eval x (eval₂ f g p) = eval₂ ((eval x) ∘ f) (λ s, eval x (g s)) p.
Русский
Для гомоморфизма f: R →+* S и семейства g: σ → MvPolynomial τ S, а также p ∈ MvPolynomial σ R верно: eval_x (eval₂ f g p) = eval₂ ((eval x) ∘ f) (λ s, eval_x(g(s))) p.
LaTeX
$$$$\operatorname{eval}_x\bigl(\operatorname{eval}_2 f g p\bigr) = \operatorname{eval}_2\bigl( (\operatorname{eval}_x) \circ f \bigr)\;\bigl( \lambda s. \operatorname{eval}_x(g(s)) \bigr)\; p.$$$$
Lean4
@[simp]
theorem eval₂_id {g : σ → R} (p : MvPolynomial σ R) : eval₂ (RingHom.id _) g p = eval g p :=
rfl
