eval_C

Mathlib.Algebra.Polynomial.Eval.Defs

URI: https://scilib.ai/kg/mathlib#Polynomial.eval_C

English

Let n ∈ ℕ with n ≥ 2 and a ∈ R. Then (ofNat(n) : R[X]).eval a = ofNat(n).

Русский

Пусть n ∈ ℕ с n ≥ 2 и a ∈ R. Тогда (ofNat(n) : R[X]).eval a = ofNat(n).

LaTeX

$$$ (\mathrm{ofNat}(n) : R[X]).\mathrm{eval}\ a = \mathrm{ofNat}(n) $$$

Lean4

@[simp]
theorem eval_C : (C a).eval x = a :=
  eval₂_C _ _

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

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

Разделы

Аффилиация

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