logDeriv_inv

Mathlib.Analysis.Calculus.LogDeriv

URI: https://scilib.ai/kg/mathlib#logDeriv_inv

English

The log-derivative of the reciprocal map x ↦ x^{-1} is -1/x.

Русский

Логарифмическая производная отображения обратного значения x ↦ x^{-1} равна -1/x.

LaTeX

$$$\displaystyle \logDeriv\bigl(x \mapsto x^{-1}\bigr)(x) = -\frac{1}{x}$$$

Lean4

@[simp]
theorem logDeriv_inv (x : 𝕜) : logDeriv (·⁻¹) x = -1 / x := by simpa using logDeriv_zpow x (-1)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru