aeval_X

Mathlib.Algebra.Polynomial.AlgebraMap

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

English

aeval x sends the indeterminate X to x.

Русский

aeval x отправляет X в x.

LaTeX

$$$$\mathrm{aeval}_x(X) = x.$$$$

Lean4

@[simp]
theorem aeval_X : aeval x (X : R[X]) = x :=
  eval₂_X _ x

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

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

Разделы

Аффилиация

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