homologyι_opcyclesToCycles — Mathlib

English

For all i, the composition homologyι i ≫ opcyclesToCycles i j equals zero.

Русский

Для всех i композиция homologyι i ≫ opcyclesToCycles i j тождественно нулю.

LaTeX

$$$K.homology\iota i ≫ K.opcyclesToCycles i j = 0$$$

Lean4

@[reassoc (attr := simp)]
theorem homologyι_opcyclesToCycles : K.homologyι i ≫ K.opcyclesToCycles i j = 0 := by
  simp only [← cancel_mono (K.iCycles j), assoc, opcyclesToCycles_iCycles, homologyι_comp_fromOpcycles, zero_comp]

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