inv_sub_inv' — Mathlib

English

Let a, b ∈ K with a ≠ 0 and b ≠ 0 in a division ring K. Then a⁻¹ − b⁻¹ = a⁻¹ · (b − a) · b⁻¹.

Русский

Пусть a, b ∈ K, где a ≠ 0 и b ≠ 0, в делительном кольце K. Тогда a⁻¹ − b⁻¹ = a⁻¹ · (b − a) · b⁻¹.

LaTeX

$$$a^{-1} - b^{-1} = a^{-1} \\cdot (b - a) \\cdot b^{-1}$, если $a \\neq 0$ и $b \\neq 0$$$

Lean4

/-- See `inv_sub_inv` for the more convenient version when `K` is commutative. -/
theorem inv_sub_inv' {a b : K} (ha : a ≠ 0) (hb : b ≠ 0) : a⁻¹ - b⁻¹ = a⁻¹ * (b - a) * b⁻¹ :=
  let _ := invertibleOfNonzero ha;
  let _ := invertibleOfNonzero hb;
  invOf_sub_invOf a b

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