fromOpcycles_eq_zero

Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

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

← MathLib Explorer

English

If i and j are not related, K.fromOpcycles i j = 0.

Русский

Если i и j не связаны отношением, то K.fromOpcycles i j = 0.

LaTeX

$$$\neg c.Rel\ i\ j \Rightarrow K.fromOpcycles i j = 0$$$

Lean4

theorem fromOpcycles_eq_zero (hij : ¬c.Rel i j) : K.fromOpcycles i j = 0 := by
  rw [← cancel_epi (K.pOpcycles i), p_fromOpcycles, comp_zero, K.shape _ _ hij]

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

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

Разделы

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

Аффилиация

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