derivative_inv — Mathlib

English

If f is invertible in PowerSeries R, then the derivative of its inverse satisfies the Leibniz rule for inverses: d(f^{-1}) = -f^{-1} ^ 2 · df.

Русский

Если f обратим в PowerSeries R, то производная от обратного удовлетворяет правилу Лейбница для обратных: (f^{-1})' = -f^{-1 2} · f'.

LaTeX

$$$ \\frac{d}{dX} f^{-1} = - (f^{-1})^{2} \\cdot \\frac{d}{dX} f$$$

Lean4

@[simp]
theorem derivative_inv {R} [CommRing R] (f : R⟦X⟧ˣ) : d⁄dX R ↑f⁻¹ = -(↑f⁻¹ : R⟦X⟧) ^ 2 * d⁄dX R f :=
  by
  apply Derivation.leibniz_of_mul_eq_one
  simp

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