eval₂_cast_comp — Mathlib

English

For f : σ → τ, c : ℤ →+* R, g : τ → R and p ∈ MvPolynomial σ ℤ, eval₂ c (g ∘ f) p = eval₂ c g (rename f p).

Русский

Пусть f : σ → τ, c : ℤ →+* R, g : τ → R и p ∈ MvPolynomial σ ℤ. Тогда eval₂ c (g ∘ f) p = eval₂ c g (rename f p).

LaTeX

$$$ \mathrm{eval}_2\ c\ (g \circ f)\ p = \mathrm{eval}_2\ c\ g\ (rename\ f\ p) $$$

Lean4

theorem eval₂_cast_comp (f : σ → τ) (c : ℤ →+* R) (g : τ → R) (p : MvPolynomial σ ℤ) :
    eval₂ c (g ∘ f) p = eval₂ c g (rename f p) :=
  (eval₂_rename c f g p).symm

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