leibniz_invOf

Mathlib.RingTheory.Derivation.Basic

URI: https://scilib.ai/kg/mathlib#Derivation.leibniz_invOf

English

If a is invertible, D(a^{-1}) = - a^{-2} D(a).

Русский

Если a является обратимым, то D(a^{-1}) = - a^{-2} D(a).

LaTeX

$$$D(a^{-1}) = - a^{-2} D(a)$$$

Lean4

theorem leibniz_invOf [Invertible a] : D (⅟a) = -⅟a ^ 2 • D a :=
  D.leibniz_of_mul_eq_one <| invOf_mul_self a

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

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

Разделы

Аффилиация

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