eval_single — Mathlib

English

Evaluating the mapped polynomial module via eval is the same as mapping the evaluation through the map.

Русский

Оценка через eval эквивалентна отображению через карту после оценки.

LaTeX

$$eval_map (f : M →ₗ[R] M') (q : PolynomialModule R M) (r : R) : eval (algebraMap R R' r) (map R' f q) = f (eval r q)$$

Lean4

@[simp]
theorem eval_single (r : R) (i : ℕ) (m : M) : eval r (single R i m) = r ^ i • m :=
  Finsupp.sum_single_index (smul_zero _)

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