aeval_endomorphism — Mathlib

English

Another restatement of the endomorphism interaction with aeval on a module.

Русский

Ещё одно утверждение о взаимодействии aeval и линейного отображения на модуле.

LaTeX

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

Lean4

theorem aeval_endomorphism {M : Type*} [AddCommGroup M] [Module R M] (f : M →ₗ[R] M) (v : M) (p : R[X]) :
    aeval f p v = p.sum fun n b => b • (f ^ n) v :=
  by
  rw [aeval_def, eval₂_eq_sum]
  exact map_sum (LinearMap.applyₗ v) _ _

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