aeval_ofReal

Mathlib.Analysis.RCLike.Lemmas

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

English

For p ∈ ℝ[X] and x ∈ ℝ, aeval(ofReal x) p equals ofReal(eval x p).

Русский

Для p ∈ ℝ[X] и x ∈ ℝ выполняется aeval(ofReal x) p = ofReal(eval x p).

LaTeX

$$$\\mathrm{aeval}(\\mathrm{ofReal}\\ x)\,p = \\mathrm{ofReal}\\(\\mathrm{eval}\\ x\\ p$$$

Lean4

theorem aeval_ofReal (p : ℝ[X]) (x : ℝ) : aeval (RCLike.ofReal x : K) p = eval x p :=
  aeval_algHom_apply RCLike.ofRealAm x p

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

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

Разделы

Аффилиация

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