leibniz_div

Mathlib.RingTheory.Derivation.Basic

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

← MathLib Explorer

English

If D(b) = 0, then D(a/b) = b^{-1} D(a).

Русский

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

LaTeX

$$$D(b) = 0 \Rightarrow D\left(\frac{a}{b}\right) = b^{-1} D(a)$$$

Lean4

theorem leibniz_div (a b : K) : D (a / b) = b⁻¹ ^ 2 • (b • D a - a • D b) :=
  by
  simp only [div_eq_mul_inv, leibniz, leibniz_inv, inv_pow, neg_smul, smul_neg, smul_smul, add_comm, sub_eq_add_neg,
    smul_add]
  rw [← inv_mul_mul_self b⁻¹, inv_inv]
  ring_nf

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

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

Разделы

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

Аффилиация

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