aevalTower_X

Mathlib.Algebra.MvPolynomial.Eval

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

English

Repeated statement about aevalTower on X_i.

Русский

Повторяющееся утверждение о aevalTower на X_i.

LaTeX

$$$$ \mathrm{aevalTower}(g,y)(X_i) = y_i $$$$

Lean4

@[simp]
theorem aevalTower_X (i : σ) : aevalTower g y (X i) = y i :=
  eval₂_X _ _ _

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

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

Разделы

Аффилиация

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