div_add_one

Mathlib.Algebra.Field.Basic

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

English

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

Русский

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

LaTeX

$$$$a/b + 1 = (a+b)/b \quad (b\neq 0).$$$$

Lean4

theorem div_add_one (h : b ≠ 0) : a / b + 1 = (a + b) / b :=
  (div_add_same h).symm

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

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

Разделы

Аффилиация

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