leval — Mathlib

English

The linear evaluation map leval r is the R-linear map sending a polynomial f to its evaluation f.eval r.

Русский

Линейное отображение оценки lev alpha на точке r — линейное отображение, сопоставляющее полином f его значение f.eval r.

LaTeX

$$$\\mathrm{leval}(r): R[X] \\to_R R,\\; f \\mapsto f.eval r$$$

Lean4

/-- `Polynomial.eval` as linear map -/
@[simps]
def leval {R : Type*} [Semiring R] (r : R) : R[X] →ₗ[R] R
    where
  toFun f := f.eval r
  map_add' _f _g := eval_add
  map_smul' c f := eval_smul c f r

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