coe_eval₂RingHom — Mathlib

English

For a ring hom f: R →+* S and x ∈ S, the evaluation map on polynomials defined via the coefficients is the same as the standard evaluation: eval₂RingHom f x = eval₂ f x as functions R[X] → S.

Русский

Для кольцеобразного гомоморфа f: R →+* S и элемента x ∈ S отображение оценки полиномов по коэффициентам совпадает с обычной оценкой: eval₂RingHom f x = eval₂ f x.

LaTeX

$$$\mathrm{coe\_eval\_2RingHom} : \forall f\,x,\; \operatorname{eval}_2^{\mathrm{RingHom}}(f,x) = \operatorname{eval}_2 f x$$$

Lean4

@[simp]
theorem coe_eval₂RingHom (f : R →+* S) (x) : ⇑(eval₂RingHom f x) = eval₂ f x :=
  rfl

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