pOpcycles_opcyclesToCycles_iCycles

English

The composition pOpcycles i ≫ opcyclesToCycles i j ≫ iCycles j equals the differential d i j in K.

Русский

Составной выражение pOpcycles i ≫ opcyclesToCycles i j ≫ iCycles j совпадает с дифференциалом d i j в K.

LaTeX

$$$K.pOpcycles i ≫ K.opcyclesToCycles i j ≫ K.iCycles j = K.d i j$$$

Lean4

@[reassoc]
theorem pOpcycles_opcyclesToCycles_iCycles : K.pOpcycles i ≫ K.opcyclesToCycles i j ≫ K.iCycles j = K.d i j := by
  simp [opcyclesToCycles]

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