eval_assoc — Mathlib

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

Похожие утверждения