eval_map'

Mathlib.Algebra.Polynomial.Module.Basic

URI: https://scilib.ai/kg/mathlib#PolynomialModule.eval_map'

English

If f is a linear map M → M, then eval r (map R f q) = f (eval r q).

Русский

Если f – линейное отображение M → M, тогда eval r (map R f q) = f (eval r q).

LaTeX

$$$\\operatorname{eval} r (\\operatorname{map} R f q) = f (\\operatorname{eval} r q)$$$

Lean4

@[simp]
theorem eval_map' (f : M →ₗ[R] M) (q : PolynomialModule R M) (r : R) : eval r (map R f q) = f (eval r q) :=
  eval_map R f q r

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru