p_fromOpcycles

Mathlib.Algebra.Homology.ShortComplex.RightHomology

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ShortComplex.p_fromOpcycles

English

The composition S.pOpcycles followed by S.fromOpcycles equals S.g.

Русский

Состав S.pOpcycles ; S.fromOpcycles равен S.g.

LaTeX

$$$ S.pOpcycles \circ S.fromOpcycles = S.g $$$

Lean4

@[reassoc (attr := simp)]
theorem p_fromOpcycles : S.pOpcycles ≫ S.fromOpcycles = S.g :=
  S.rightHomologyData.p_g'

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

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

Разделы

Аффилиация

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