sub_zero

Mathlib.CategoryTheory.Abelian.NonPreadditive

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

← MathLib Explorer

English

In a non-preadditive abelian setting, a - 0 = a.

Русский

В негладко-аддитивной абелевой обстановке, a − 0 = a.

LaTeX

$$$a - 0 = a$$$

Lean4

theorem sub_zero {X Y : C} (a : X ⟶ Y) : a - 0 = a :=
  by
  rw [sub_def]
  conv_lhs =>
    congr; congr; rw [← Category.comp_id a]
    case a.g => rw [show 0 = a ≫ (0 : Y ⟶ Y) by simp]
  rw [← prod.comp_lift, Category.assoc, lift_σ, Category.comp_id]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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