taylor_coeff_one

Mathlib.Algebra.Polynomial.Taylor

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

English

The 1-st coefficient equals f'.eval r.

Русский

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

LaTeX

$$$$ (\operatorname{taylor} r f)_{1} = f'.{\mathrm{eval}}(r) $$$$

Lean4

@[simp]
theorem taylor_coeff_one : (taylor r f).coeff 1 = f.derivative.eval r := by rw [taylor_coeff, hasseDeriv_one]

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

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

Разделы

Аффилиация

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