eval₂_comp — Mathlib

English

Let f: R →+* S1, g: σ → R, p ∈ MvPolynomial σ R. Then applying f after evaluating p with g is the same as evaluating p with the composite g followed by f. In symbols, f (eval g p) = eval₂ f (f ∘ g) p.

Русский

Пусть f: R →+* S1, g: σ → R, p ∈ MvPolynomial(σ, R). Тогда применение f к результату оценки p по g равно оценке p через составной образ g затем f: f(eval g p) = eval₂ f (f ∘ g) p.

LaTeX

$$$f\\\\left(\\\\mathrm{eval}\\\\, g \\, p\\\\right) = \\\\\\mathrm{eval}_2 f (f \\\\\\circ g) p$$$

Lean4

theorem eval₂_comp (f : R →+* S₁) (g : σ → R) (p : MvPolynomial σ R) : f (eval g p) = eval₂ f (f ∘ g) p := by
  rw [← p.map_id, eval_map, eval₂_comp_right]

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