eval₂Hom_map_hom — Mathlib

English

For f: R →+* S1, g: σ → S2, φ: S1 →+* S2, p ∈ MvPolynomial σ R, the map version with homs satisfies eval₂Hom φ g (map f p) = eval₂Hom (φ ∘ f) g p.

Русский

Для f: R →+* S1, g: σ → S2, φ: S1 →+* S2, p ∈ MvPolynomial σ R, верно: eval₂Hom φ g (map f p) = eval₂Hom (φ ∘ f) g p.

LaTeX

$$$\\\\mathrm{eval}_2\\\\mathrm{Hom} \\\\phi g (\\\\mathrm{map}_f p) = \\\\mathrm{eval}_2\\\\mathrm{Hom} (\\\\phi \\\\circ f) g p$$$

Lean4

@[simp]
theorem eval₂Hom_map_hom [CommSemiring S₂] (f : R →+* S₁) (g : σ → S₂) (φ : S₁ →+* S₂) (p : MvPolynomial σ R) :
    eval₂Hom φ g (map f p) = eval₂Hom (φ.comp f) g p :=
  eval₂_map f g φ p

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