leval_coe_eq_smeval — Mathlib

English

The evaluation operator leval r coincides with smeval.linearMap R r; that is, leval r = smeval.linearMap R r.

Русский

Оператор оценки leval r совпадает с smeval.linearMap R r; то есть leval r = smeval.linearMap R r.

LaTeX

$$$$ \forall R [\mathrm{Semiring} R], \forall r \in R, leval\ r = smeval.linearMap\ R\ r. $$$$

Lean4

theorem leval_coe_eq_smeval {R : Type*} [Semiring R] (r : R) : ⇑(leval r) = fun p => p.smeval r :=
  by
  rw [funext_iff]
  intro
  rw [leval_apply, smeval_def, eval_eq_sum]
  rfl

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