sub_self

Mathlib.CategoryTheory.Abelian.NonPreadditive

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

English

In a non-preadditive abelian category, a − a = 0.

Русский

В абелевой категории без предварительного дополнения, a − a = 0.

LaTeX

$$$a - a = 0$$$

Lean4

theorem sub_self {X Y : C} (a : X ⟶ Y) : a - a = 0 := by
  rw [sub_def, ← Category.comp_id a, ← prod.comp_lift, Category.assoc, diag_σ, comp_zero]

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

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

Разделы

Аффилиация

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