dFrom_comp_xNextIso

Mathlib.Algebra.Homology.HomologicalComplex

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

← MathLib Explorer

English

For r: c.Rel i j, the composition of dFrom i with (xNextIso r).hom equals d i j.

Русский

Для r: c.Rel i j композиция dFrom i с (xNextIso r).hom равна d i j.

LaTeX

$$$\\\\; C.dFrom i \\\\circ (C.xNextIso r).hom = C.d i j$$$

Lean4

@[reassoc (attr := simp)]
theorem dFrom_comp_xNextIso {i j : ι} (r : c.Rel i j) : C.dFrom i ≫ (C.xNextIso r).hom = C.d i j := by
  simp [C.dFrom_eq r]

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

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

Разделы

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

Аффилиация

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