inv_sub_inv

Mathlib.Algebra.Field.Basic

URI: https://scilib.ai/kg/mathlib#inv_sub_inv

← MathLib Explorer

English

Let a,b ∈ K with a ≠ 0, b ≠ 0. Then a⁻¹ − b⁻¹ = (b − a)/(a b).

Русский

Пусть a,b ∈ K, a ≠ 0, b ≠ 0. Тогда a⁻¹ − b⁻¹ = (b − a)/(a b).

LaTeX

$$$a^{-1} - b^{-1} = \\dfrac{b - a}{a b}$, при $a \\neq 0$, $b \\neq 0$$$

Lean4

theorem inv_sub_inv {a b : K} (ha : a ≠ 0) (hb : b ≠ 0) : a⁻¹ - b⁻¹ = (b - a) / (a * b) := by
  rw [inv_eq_one_div, inv_eq_one_div, div_sub_div _ _ ha hb, one_mul, mul_one]

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

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

Разделы

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

Аффилиация

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