same_sub_div

Mathlib.Algebra.Field.Basic

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

English

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

Русский

При b ≠ 0, (b − a)/b = 1 − a/b.

LaTeX

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

Lean4

theorem same_sub_div {a b : K} (h : b ≠ 0) : (b - a) / b = 1 - a / b := by
  simpa only [← @div_self _ _ b h] using (div_sub_div_same b a b).symm

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

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

Разделы

Аффилиация

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