leibniz_inv

Mathlib.RingTheory.Derivation.Basic

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

← MathLib Explorer

English

If a,b ∈ K with b ≠ 0, then D(a/b) = b^{-1}^2 ( b D(a) − a D(b) ).

Русский

Если a,b ∈ K, b ≠ 0, то D(a/b) = b^{-1}^2 ( b D(a) − a D(b) ).

LaTeX

$$$D\left(\frac{a}{b}\right) = b^{-2} ( b D(a) - a D(b) )$$$

Lean4

theorem leibniz_inv (a : K) : D a⁻¹ = -a⁻¹ ^ 2 • D a :=
  by
  rcases eq_or_ne a 0 with (rfl | ha)
  · simp
  · exact D.leibniz_of_mul_eq_one (inv_mul_cancel₀ ha)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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