d_toCycles — Mathlib

English

For i, j, k and [K.HasHomology i], we have d_i_j followed by toCycles j k equals zero: K.d i j ≫ K.toCycles j k = 0.

Русский

Для индексов i, j, k и при наличии i-гомологий, композиция d_i_j затем toCycles j k равна нулю: K.d i j ≫ K.toCycles j k = 0.

LaTeX

$$$K.d\ i\ j \circ K.toCycles\ j\ k = 0$$$

Lean4

@[reassoc (attr := simp)]
theorem d_toCycles [K.HasHomology k] : K.d i j ≫ K.toCycles j k = 0 := by
  simp only [← cancel_mono (K.iCycles k), assoc, toCycles_i, d_comp_d, zero_comp]

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