div_sub_div_same

Mathlib.Algebra.Field.Basic

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

English

For a,b,c in K, a/c − b/c = (a − b)/c.

Русский

Для a,b,c в K: a/c − b/c = (a − b)/c.

LaTeX

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

Lean4

theorem div_sub_div_same (a b c : K) : a / c - b / c = (a - b) / c := by
  rw [sub_eq_add_neg, ← neg_div, ← add_div, sub_eq_add_neg]

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

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

Разделы

Аффилиация

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