zero_comp

Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.zero_comp

English

Composition with a zero morphism on the left yields the zero morphism: 0 ≫ f = 0.

Русский

Составление слева с нулевой морфизмом даёт нулевой морфизм: 0 ≫ f = 0.

LaTeX

$$$0 \\circ f = 0$$$

Lean4

@[simp]
theorem zero_comp [HasZeroMorphisms C] {X : C} {Y Z : C} {f : Y ⟶ Z} : (0 : X ⟶ Y) ≫ f = (0 : X ⟶ Z) :=
  HasZeroMorphisms.zero_comp X f

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

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

Разделы

Аффилиация

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