neg_div_self

Mathlib.Algebra.Field.Basic

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

English

If a,b ≠ 0 and commute, then a^{-1} + b^{-1} = (a + b)/(ab).

Русский

Если a,b ≠ 0 и коммутируют, то a^{-1} + b^{-1} = (a + b)/(ab).

LaTeX

$$$$a^{-1} + b^{-1} = \frac{a+b}{ab} \quad (a,b\neq 0,\; \text{Commute}(a,b)).$$$$

Lean4

@[simp]
theorem neg_div_self {a : K} (h : a ≠ 0) : -a / a = -1 := by rw [neg_div, div_self h]

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

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

Разделы

Аффилиация

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