opcyclesToCycles_iCycles — Mathlib

English

For a complex K, the relation opcyclesToCycles_iCycles holds: K.opcyclesToCycles i j ≫ K.iCycles j = K.fromOpcycles i j.

Русский

Для комплекса K выполняется тождество: K.opcyclesToCycles i j ≫ K.iCycles j = K.fromOpcycles i j.

LaTeX

$$$K.{opcyclesToCycles i j} \;\; \;\; \; ≫ K.{iCycles j} = K.{fromOpcycles i j}$$$

Lean4

@[reassoc (attr := simp)]
theorem opcyclesToCycles_iCycles : K.opcyclesToCycles i j ≫ K.iCycles j = K.fromOpcycles i j :=
  by
  dsimp only [opcyclesToCycles]
  simp

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