eval_map_algebraMap

Mathlib.Algebra.Polynomial.AlgebraMap

URI: https://scilib.ai/kg/mathlib#Polynomial.eval_map_algebraMap

English

For P in R[X] and b in B, eval at b of the image of P under algebra map equals aeval b applied to P.

Русский

Для P в R[X] и b в B, значение (map (algebraMap R B) P) в b равно aeval_b(P).

LaTeX

$$$$\mathrm{eval}\,b\bigl(\mathrm{map}(\mathrm{algebraMap}\ R B)\, P\bigr) = \mathrm{aeval}_b\, P.$$$$

Lean4

@[simp]
theorem eval_map_algebraMap (P : R[X]) (b : B) : (map (algebraMap R B) P).eval b = aeval b P := by
  rw [aeval_def, eval_map]

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

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

Разделы

Аффилиация

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