sub_add

Mathlib.CategoryTheory.Abelian.NonPreadditive

URI: https://scilib.ai/kg/mathlib#CategoryTheory.NonPreadditiveAbelian.sub_add

English

For any a, b, -(a + b) = (−a) + (−b).

Русский

Для любых a, b: -(a + b) = (−a) + (−b).

LaTeX

$$$ -(a + b) = (-a) + (-b) $$$

Lean4

theorem sub_add {X Y : C} (a b c : X ⟶ Y) : a - b + c = a - (b - c) := by rw [add_def, neg_def, sub_sub_sub, sub_zero]

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

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

Разделы

Аффилиация

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