iterate_derivative_neg

Mathlib.Algebra.Polynomial.Derivative

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

English

For any f and k, derivative iterated k times of −f equals the negation of derivative iterated k times of f.

Русский

Для любого f и k, k-раз производная от −f равна − k-раз производной от f.

LaTeX

$$$\operatorname{derivative}^{[k]}(-f) = -\operatorname{derivative}^{[k]} f$$$

Lean4

theorem iterate_derivative_neg {f : R[X]} {k : ℕ} : derivative^[k] (-f) = -derivative^[k] f :=
  iterate_map_neg derivative k f

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

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

Разделы

Аффилиация

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