toCycles_eq_zero

Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

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

← MathLib Explorer

English

If i and j are not related in the complex shape, then K.toCycles i j = 0.

Русский

Если i и j не связаны отношением в форме сложной структуры, то K.toCycles i j = 0.

LaTeX

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

Lean4

theorem toCycles_eq_zero [K.HasHomology j] (hij : ¬c.Rel i j) : K.toCycles i j = 0 := by
  rw [← cancel_mono (K.iCycles j), toCycles_i, zero_comp, K.shape _ _ hij]

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

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

Разделы

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

Аффилиация

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