eval₂_comp_left — Mathlib

English

Let k : S1 →+* S2 be a ring hom and f : R →+* S1, g : σ → S1. For any p ∈ MvPolynomial σ R, we have k(eval₂ f g p) = eval₂ (k ∘ f) (k ∘ g) p.

Русский

Пусть k : S1 →+* S2 — кольцевой гомоморф, f : R →+* S1, g : σ → S1. Для любого p ∈ MvPolynomial σ R верно: k( eval₂ f g p ) = eval₂ (k ∘ f) (k ∘ g) p.

LaTeX

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

Lean4

theorem eval₂_comp_left {S₂} [CommSemiring S₂] (k : S₁ →+* S₂) (f : R →+* S₁) (g : σ → S₁) (p) :
    k (eval₂ f g p) = eval₂ (k.comp f) (k ∘ g) p := by
  apply MvPolynomial.induction_on p <;> simp +contextual [eval₂_add, k.map_add, eval₂_mul, k.map_mul]

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