eval_eq_smeval — Mathlib

English

Let R be a semiring and p be a polynomial over R. For every r in R, the standard evaluation of p at r coincides with the smeval evaluation at r; i.e., p.eval r = p.smeval r.

Русский

Пусть R — полукольцо и p — полином над R. Для любого r ∈ R обычная подстановка p на r совпадает с вычислением smeval на r; то есть p.eval r = p.smeval r.

LaTeX

$$$$ \forall (R : Type*) [\mathrm{Semiring}~R] (r : R) (p : R[X]), p.eval r = p.smeval r. $$$$

Lean4

theorem eval_eq_smeval : p.eval r = p.smeval r :=
  by
  rw [eval_eq_sum, smeval_eq_sum]
  rfl

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