iteratedDeriv_one

Mathlib.Analysis.Calculus.IteratedDeriv.Defs

URI: https://scilib.ai/kg/mathlib#iteratedDeriv_one

English

The first iterated derivative equals the ordinary derivative: iteratedDeriv 1 f = deriv f.

Русский

Первая итеративная производная равна обычной производной: iteratedDeriv 1 f = deriv f.

LaTeX

$$$\operatorname{iteratedDeriv} 1\ f = \operatorname{deriv} f$$$

Lean4

@[simp]
theorem iteratedDeriv_one : iteratedDeriv 1 f = deriv f := by ext x; simp [iteratedDeriv]

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

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

Разделы

Аффилиация

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