π₁Toπ₂_comp_π₂Toπ₃

Mathlib.Algebra.Homology.ShortComplex.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ShortComplex.π₁Toπ₂_comp_π₂Toπ₃

English

The composition (π1Toπ2) ≫ (π2Toπ3) equals zero.

Русский

Составление (π1Toπ2) и (π2Toπ3) равно нулю.

LaTeX

$$$$ (\\pi_1To\\pi_2) \\;\\; ≫ \\;\\; (\\pi_2To\\pi_3) = 0. $$$$

Lean4

@[reassoc (attr := simp)]
theorem π₁Toπ₂_comp_π₂Toπ₃ : (π₁Toπ₂ : (_ : _ ⥤ C) ⟶ _) ≫ π₂Toπ₃ = 0 := by cat_disch

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

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

Разделы

Аффилиация

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