eval₂RingHom — Mathlib

English

Again, finsupp-based evaluation equals liftNC application.

Русский

Ещё одно, оценка finsupp-полинома равна применению liftNC.

LaTeX

$$$\operatorname{ev}_{f,x}\{ toFinsupp := p \} = \operatorname{liftNC}(\uparrow f)(\text{powersHom } S\ x) p$$$

Lean4

/-- `eval₂` as a `RingHom` -/
def eval₂RingHom (f : R →+* S) (x : S) : R[X] →+* S :=
  { eval₂AddMonoidHom f x with
    map_one' := eval₂_one _ _
    map_mul' := fun _ _ => eval₂_mul _ _ }

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