English
Let f: R →+* S1, g: σ → S2, φ: S1 →+* S2, p ∈ MvPolynomial σ R. Evaluating after mapping p with f against φ is the same as mapping p via φ ∘ f before evaluating with g. In symbols, eval₂ φ g (map f p) = eval₂ (φ ∘ f) g p.
Русский
Пусть f: R →+* S1, g: σ → S2, φ: S1 →+* S2, p ∈ MvPolynomial σ R. Тогда выполняется: eval₂ φ g (map f p) = eval₂ (φ ∘ f) g p.
LaTeX
$$$\\\\mathrm{eval}_2\\\\, φ\\\\, g \\\\left(\\\\mathrm{map}_f p\\\\right) = \\\\mathrm{eval}_2 (\\\\phi \\\\circ f) g p$$$
Lean4
@[simp]
theorem eval₂_map [CommSemiring S₂] (f : R →+* S₁) (g : σ → S₂) (φ : S₁ →+* S₂) (p : MvPolynomial σ R) :
eval₂ φ g (map f p) = eval₂ (φ.comp f) g p := by rw [← eval_map, ← eval_map, map_map]
