eval_ofNat

Mathlib.Algebra.Polynomial.Eval.Defs

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

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_ofNat (n : ℕ) [n.AtLeastTwo] (a : R) : (ofNat(n) : R[X]).eval a = ofNat(n) := by
  simp only [OfNat.ofNat, eval_natCast]

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

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

Разделы

Аффилиация

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