sub_div

Mathlib.Algebra.Field.Basic

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

English

Let K be a division ring. For all a, b, c in K, the division by c distributes over subtraction: (a − b)/c = a/c − b/c.

Русский

Пусть K - делительный кольцо. Для любых a, b, c ∈ K выполняется: (a − b)/c = a/c − b/c.

LaTeX

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

Lean4

theorem sub_div (a b c : K) : (a - b) / c = a / c - b / c :=
  (div_sub_div_same _ _ _).symm

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

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

Разделы

Аффилиация

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