opcyclesToCycles_homologyπ — Mathlib

English

The composition opcyclesToCycles i j ≫ homologyπ j is zero.

Русский

Составной операторы opcyclesToCycles i j и homologyπ j дают нулевой композиционный результат.

LaTeX

$$$K.opcyclesToCycles i j ≫ K.homologyπ j = 0$$$

Lean4

@[reassoc (attr := simp)]
theorem opcyclesToCycles_homologyπ : K.opcyclesToCycles i j ≫ K.homologyπ j = 0 := by
  simp only [← cancel_epi (K.pOpcycles i), pOpcycles_opcyclesToCycles_assoc, toCycles_comp_homologyπ, comp_zero]

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