p_fromOpcycles

Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

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

English

The composition of pOpcycles with fromOpcycles equals the differential: K.pOpcycles i ≫ K.fromOpcycles i j = K.d i j.

Русский

Составление pOpcycles и fromOpcycles дает дифференциал: K.pOpcycles i ≫ K.fromOpcycles i j = K.d i j.

LaTeX

$$$K.pOpcycles i \circ K.fromOpcycles i j = K.d i j$$$

Lean4

@[reassoc (attr := simp)]
theorem p_fromOpcycles : K.pOpcycles i ≫ K.fromOpcycles i j = K.d i j :=
  p_descOpcycles _ _ _ _ _

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

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

Разделы

Аффилиация

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