inv_add_inv

Mathlib.Algebra.Field.Basic

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

English

Let a,b ∈ semifield with a,b ≠ 0. Then a⁻¹ + b⁻¹ = (a + b)/(ab).

Русский

Пусть a,b ∈ полуполевая, оба не нуль. Тогда a⁻¹ + b⁻¹ = (a + b)/(ab).

LaTeX

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

Lean4

theorem inv_add_inv (ha : a ≠ 0) (hb : b ≠ 0) : a⁻¹ + b⁻¹ = (a + b) / (a * b) :=
  (Commute.all a _).inv_add_inv ha hb

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

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

Разделы

Аффилиация

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