one_add_div

Mathlib.Algebra.Field.Basic

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

English

For nonzero a,b in a division semiring, (1/a)·(a+b)·(1/b) = (1/a) + (1/b).

Русский

Для ненулевых a,b в полукольце деления: (1/a)·(a+b)·(1/b) = (1/a) + (1/b).

LaTeX

$$$$\frac{1}{a}\cdot (a+b)\cdot \frac{1}{b} = \frac{1}{a} + \frac{1}{b}\quad(a\neq 0,b\neq 0).$$$$

Lean4

theorem one_add_div (h : b ≠ 0) : 1 + a / b = (b + a) / b :=
  (same_add_div h).symm

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

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

Разделы

Аффилиация

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