aevalTower_ofId

Mathlib.Algebra.MvPolynomial.Eval

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

← MathLib Explorer

English

For every Nat n ≥ 2, aevalTower g y (ofNat(n)) = ofNat(n).

Русский

Для любого натурального n ≥ 2 выполняется aevalTower g y (ofNat(n)) = ofNat(n).

LaTeX

$$$$ \operatorname{aevalTower}(g,y)(\operatorname{ofNat}(n)) = \operatorname{ofNat}(n). $$$$

Lean4

@[simp]
theorem aevalTower_ofId : aevalTower (Algebra.ofId S A) = (aeval : (σ → A) → MvPolynomial σ S →ₐ[S] A) :=
  by
  ext
  simp only [aeval_X, aevalTower_X]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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