aeval_X_left_apply

Mathlib.Algebra.MvPolynomial.Eval

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

English

For any polynomial p in MvPolynomial(σ, R), evaluating with X yields p.

Русский

Для любого многочлена p ∈ MvPolynomial(σ, R) оценивание по X возвращает сам p.

LaTeX

$$$$ \mathrm{aeval}_X(p) = p $$$$

Lean4

theorem aeval_X_left_apply (p : MvPolynomial σ R) : aeval X p = p :=
  AlgHom.congr_fun aeval_X_left p

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

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

Разделы

Аффилиация

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