taylor_coeff_zero

Mathlib.Algebra.Polynomial.Taylor

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

English

The 0-th coefficient equals f.eval r.

Русский

0-й коэффициент равен f.eval r.

LaTeX

$$$$ (\operatorname{taylor} r f)_{0} = f(r) $$$$

Lean4

@[simp]
theorem taylor_coeff_zero : (taylor r f).coeff 0 = f.eval r := by rw [taylor_coeff, hasseDeriv_zero, LinearMap.id_apply]

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

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

Разделы

Аффилиация

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