taylor_eval_sub

Mathlib.Algebra.Polynomial.Taylor

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

English

For r ∈ R and f ∈ R[X], (taylor r f).eval (s − r) = f.eval s for all s ∈ R.

Русский

Для r ∈ R и f ∈ R[X] выполняется (taylor r f).eval (s − r) = f.eval s для всех s ∈ R.

LaTeX

$$$$ (\\operatorname{taylor}(r,f)).\\mathrm{eval}(s - r) = f.\\mathrm{eval}(s). $$$$

Lean4

theorem taylor_eval_sub (s : R) : (taylor r f).eval (s - r) = f.eval s := by rw [taylor_eval, sub_add_cancel]

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

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

Разделы

Аффилиация

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