leibniz_of_mul_eq_one — Mathlib

English

If a and b are elements with a·b = 1, then D(a) = - a^2 D(b).

Русский

Если a · b = 1, то D(a) = - a^2 D(b).

LaTeX

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

Lean4

theorem leibniz_of_mul_eq_one {a b : A} (h : a * b = 1) : D a = -a ^ 2 • D b :=
  by
  rw [neg_smul]
  refine eq_neg_of_add_eq_zero_left ?_
  calc
    D a + a ^ 2 • D b = a • b • D a + a • a • D b := by simp only [smul_smul, h, one_smul, sq]
    _ = a • D (a * b) := by rw [leibniz, smul_add, add_comm]
    _ = 0 := by rw [h, map_one_eq_zero, smul_zero]

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