aeval_neg — Mathlib

English

For a linear endomorphism f of a module M over R and a polynomial p, the value aeval f p v equals the finite sum of coefficients of p times powers of f applied to v.

Русский

Для линейного эндоморфизма f модуля M над R и многочлена p выполняется: aeval f p v = ∑ coeff_i(p) · f^i(v).

LaTeX

$$aeval_endomorphism f v p = p.sum (fun n b => b • (f ^ n) v)$$

Lean4

@[simp]
theorem aeval_neg {p : R[X]} [Ring A] [Algebra R A] (x : A) : aeval x (-p) = -aeval x p :=
  map_neg ..

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