derivative_inv' — Mathlib

English

For fields, the derivative of the inverse for a unit in the power-series ring satisfies the formula with the inverse; under the invertibility assumption the same holds.

Русский

Для полей производная обратного для единицы в кольце степенных рядов удовлетворяет формуле с обратным элементом; при предположении обратимости — то же самое.

LaTeX

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

Lean4

@[simp]
theorem derivative_inv' {R} [Field R] (f : R⟦X⟧) : d⁄dX R f⁻¹ = -f⁻¹ ^ 2 * d⁄dX R f :=
  by
  by_cases h : constantCoeff f = 0
  · suffices f⁻¹ = 0 by rw [this, pow_two, zero_mul, neg_zero, zero_mul, map_zero]
    rwa [MvPowerSeries.inv_eq_zero]
  apply Derivation.leibniz_of_mul_eq_one
  exact PowerSeries.inv_mul_cancel (h := h)

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