iter_deriv_inv_linear_sub — Mathlib

English

A variant for (c x − d)^{-1}: the k-th derivative is (-1)^k k! c^k (c x − d)^{-(1+k)}.

Русский

Вариант для (c x − d)^{-1}: k-я производная равна (-1)^k k! c^k (c x − d)^{-(1+k)}.

LaTeX

$$$\\mathrm{deriv}^[k] (x \\mapsto (c x - d)^{-1}) = (-1)^k k! \\cdot c^k \\cdot (c x - d)^{-(1+k)}$$$

Lean4

theorem iter_deriv_inv_linear_sub (k : ℕ) (c d : 𝕜) :
    deriv^[k] (fun x ↦ (c * x - d)⁻¹) = (fun x : 𝕜 ↦ (-1) ^ k * k ! * c ^ k * (c * x - d) ^ (-1 - k : ℤ)) := by
  simpa [sub_eq_add_neg] using iter_deriv_inv_linear k c (-d)

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