fromOpcycles_d

Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

URI: https://scilib.ai/kg/mathlib#HomologicalComplex.fromOpcycles_d

← MathLib Explorer

English

For all i, j, k, K.fromOpcycles i j ≫ K.d j k = 0.

Русский

Для любых i, j, k вещественное: fromOpcycles i j ⋯ d j k = 0.

LaTeX

$$$K.fromOpcycles i j \circ K.d j k = 0$$$

Lean4

@[reassoc (attr := simp)]
theorem fromOpcycles_d : K.fromOpcycles i j ≫ K.d j k = 0 := by
  simp only [← cancel_epi (K.pOpcycles i), p_fromOpcycles_assoc, d_comp_d, comp_zero]

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

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

Разделы

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

Аффилиация

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