English
If f is invertible in PowerSeries over a commutative ring and the base ring is a field, the derivative of the inverse satisfies the same formula as in the field case: d f^{-1} = -f^{-2} · df.
Русский
Если f обратим в PowerSeries над коммутативной кольцом и основание — поле, то производная обратного ряда удовлетворяет той же формуле: (f^{-1})' = -f^{-2} · f'.
LaTeX
$$$ \\frac{d}{dX} f^{-1} = - f^{-1}^2 \\cdot \\frac{d}{dX} f$$$
Lean4
@[simp]
theorem derivative_invOf {R} [CommRing R] (f : R⟦X⟧) [Invertible f] : d⁄dX R ⅟f = -⅟f ^ 2 * d⁄dX R f := by
rw [Derivation.leibniz_invOf, smul_eq_mul]
/-
The following theorem is stated only in the case that `R` is a field. This is because
there is currently no instance of `Inv R⟦X⟧` for more general base rings `R`.
-/
