aeval_X

Mathlib.Algebra.MvPolynomial.Eval

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

English

The evaluation sends the indeterminate X_s to its image under f: aeval f (X_s) = f(s).

Русский

Оценивание отправляет переменную X_s в образ f(s): aeval f (X_s) = f(s).

LaTeX

$$$\\\\mathrm{aeval} f (X_s) = f s$$$

Lean4

@[simp]
theorem aeval_X (s : σ) : aeval f (X s : MvPolynomial _ R) = f s :=
  eval₂_X _ _ _

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

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

Разделы

Аффилиация

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