aeval_ofNat

Mathlib.Algebra.MvPolynomial.Eval

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

English

For natural numbers n with an appropriate proof-structure, evaluating the natural polynomial of n yields the natural in S1: aeval f (ofNat(n)) = ofNat(n).

Русский

Для натурального числа n верно: aeval f (ofNat(n)) = ofNat(n).

LaTeX

$$$\\\\mathrm{aeval} f (\\\\mathrm{ofNat}(n)) = \\\\mathrm{ofNat}(n)$$$

Lean4

@[simp]
theorem aeval_ofNat (n : Nat) [n.AtLeastTwo] : aeval f (ofNat(n) : MvPolynomial σ R) = ofNat(n) :=
  map_ofNat _ _

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

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

Разделы

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

Аффилиация

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