div_add_div_same

Mathlib.Algebra.Field.Basic

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

English

For a, b, c in a division semiring, with c ≠ 0, we have a/c + b/c = (a + b)/c.

Русский

Для a, b, c в полукольце деления, при c ≠ 0 имеем a/c + b/c = (a + b)/c.

LaTeX

$$$$a/c + b/c = (a+b)/c\quad( c\neq 0),$$$$

Lean4

@[deprecated add_div (since := "2025-08-25")]
theorem div_add_div_same (a b c : K) : a / c + b / c = (a + b) / c :=
  (add_div _ _ _).symm

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

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

Разделы

Аффилиация

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