iter_deriv_inv'

Mathlib.Analysis.Calculus.Deriv.ZPow

URI: https://scilib.ai/kg/mathlib#iter_deriv_inv'

English

A simplified form: deriv^[k] Inv.inv = (-1)^k k! x^{-(1+k)} as a function of x.

Русский

Упрощенная форма: deriv^[k] Inv.inv = (-1)^k k! x^{-(1+k)}.

LaTeX

$$$\\text{deriv}'^{[k]} (x \\mapsto x^{-1}) = (-1)^k k! \\cdot x^{-(1+k)}$$$

Lean4

@[simp]
theorem iter_deriv_inv' (k : ℕ) : deriv^[k] Inv.inv = fun x : 𝕜 => (-1) ^ k * k ! * x ^ (-1 - k : ℤ) :=
  funext (iter_deriv_inv k)

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

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

Разделы

Аффилиация

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