div_sub_one

Mathlib.Algebra.Field.Basic

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

English

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

Русский

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

LaTeX

$$$$\frac{a}{b} - 1 = \frac{a-b}{b}.$$$$

Lean4

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

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

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

Разделы

Аффилиация

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