same_add_div

Mathlib.Algebra.Field.Basic

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

English

If b ≠ 0, then (b + a)/b = 1 + a/b.

Русский

Если b ≠ 0, тогда (b + a)/b = 1 + a/b.

LaTeX

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

Lean4

theorem same_add_div (h : b ≠ 0) : (b + a) / b = 1 + a / b := by rw [← div_self h, add_div]

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

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

Разделы

Аффилиация

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