one_sub_div

Mathlib.Algebra.Field.Basic

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

English

For b ≠ 0, 1 − a/b = (b − a)/b.

Русский

Для b ≠ 0, 1 − a/b = (b − a)/b.

LaTeX

$$$$1 - \frac{a}{b} = \frac{b-a}{b} \quad (b\neq 0).$$$$

Lean4

theorem one_sub_div {a b : K} (h : b ≠ 0) : 1 - a / b = (b - a) / b :=
  (same_sub_div h).symm

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

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

Разделы

Аффилиация

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