complex_d_comp

Mathlib.CategoryTheory.Preadditive.Injective.Resolution

URI: https://scilib.ai/kg/mathlib#CategoryTheory.InjectiveResolution.complex_d_comp

English

The composition d_n (n+1) ; d_{n+1} (n+2) is zero: d_n (n+1) ≫ d_{n+1} (n+2) = 0.

Русский

Сложение дифференциалов дн(н+1) и д{n+1}(n+2) равно нулю: d_n(n+1) ≫ d_{n+1}(n+2) = 0.

LaTeX

$$$$d_n^{\\;}{(n+1)} \\; \\circ d_{n+1}^{\\;}{(n+2)} = 0.$$$$

Lean4

theorem complex_d_comp (n : ℕ) : I.cocomplex.d n (n + 1) ≫ I.cocomplex.d (n + 1) (n + 2) = 0 := by simp

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

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

Разделы

Аффилиация

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