comp_eq_aeval

Mathlib.Algebra.Polynomial.AlgebraMap

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

English

aeval respects composition: aeval x (p.comp q) = aeval (aeval x q) p.

Русский

aeval сохраняет композицию: aeval x (p.comp q) = aeval (aeval x q) p.

LaTeX

$$$$\mathrm{aeval}_x(\,p.\mathrm{comp}\ q) = \mathrm{aeval}_{\mathrm{aeval}_x(q)}(p).$$$$

Lean4

theorem comp_eq_aeval : p.comp q = aeval q p :=
  rfl

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

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

Разделы

Аффилиация

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