iteratedDeriv_zero

Mathlib.Analysis.Calculus.IteratedDeriv.Defs

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

English

Zero-th iterated derivative equals the function: iteratedDeriv 0 f = f.

Русский

Нулевая итеративная производная равна функции: iteratedDeriv 0 f = f.

LaTeX

$$$\operatorname{iteratedDeriv} 0\ f = f$$$

Lean4

@[simp]
theorem iteratedDeriv_zero : iteratedDeriv 0 f = f := by ext x; simp [iteratedDeriv]

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

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

Разделы

Аффилиация

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