aeval_def

Mathlib.Algebra.Polynomial.AlgebraMap

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

English

aeval x p equals eval₂ (algebraMap R A) x p.

Русский

aeval x p равно eval₂(алгебра_map R A) x p.

LaTeX

$$$$aeval\ x\ p = eval_2(\mathrm{algebraMap}\ R\ A)\ x\ p.$$$$

Lean4

theorem aeval_def (p : R[X]) : aeval x p = eval₂ (algebraMap R A) x p :=
  rfl

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

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

Разделы

Аффилиация

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