eval₂_intCastRingHom_X — Mathlib

English

For any ring R, polynomial p with integer coefficients, and ring hom f : ℤ[X] →+* R, evaluating p with Int.castRingHom R at f X yields f p.

Русский

Для кольца R, полинома p над ℤ и кольцевого гомомора f: ℤ[X] →+* R, вычисление p при помощи Int.castRingHom R и f X даёт f p.

LaTeX

$$eval₂ (Int.castRingHom R) (f X) p = f p$$

Lean4

@[simp]
theorem eval₂_intCastRingHom_X {R : Type*} [Ring R] (p : ℤ[X]) (f : ℤ[X] →+* R) :
    eval₂ (Int.castRingHom R) (f X) p = f p :=
  eval₂_algebraMap_X p f.toIntAlgHom

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