fderiv_inverse — Mathlib

English

For a finite product ∏_{i∈u} g_i(x) of differentiable maps g_i with derivatives g'_i, the derivative is the sum over i of the product of the other factors, multiplied by g'_i, with appropriate indexing.

Русский

Для конечного произведения ∏_{i∈u} g_i(x) функций, дифференцируемых в x, производная равна сумме по i∈u от произведения остальных факторов, умноженного на производную g_i.

LaTeX

$$$\text{HasStrictFDerivAt } (\lambda x, \prod_{i∈u} g_i(x)) (\sum i ∈ u, (\prod j∈u.erase i, g_j(x)) · g'_i) x.$$$

Lean4

theorem fderiv_inverse (x : Rˣ) : fderiv 𝕜 (@Ring.inverse R _) x = -mulLeftRight 𝕜 R ↑x⁻¹ ↑x⁻¹ :=
  (hasFDerivAt_ringInverse x).fderiv

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