linearMap — Mathlib

English

The statement leval r = smeval.linearMap R r holds; equivalently, the linear maps agree on all polynomials.

Русский

Утверждение leval r = smeval.linearMap R r справедливо; эквивалентно согласованию линейных отображений на всех полиномах.

LaTeX

$$$$ leval\ r = smeval.linearMap\ R\ r. $$$$

Lean4

theorem linearMap {R : Type*} [Semiring R] (r : R) : leval r = smeval.linearMap R r :=
  by
  refine LinearMap.ext ?_
  intro
  rw [leval_apply, smeval.linearMap_apply, eval_eq_smeval]

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