of_d_ne — Mathlib

English

In the inductively constructed ChainComplex with differentials d(n+1) ∘ d(n) = 0, the matrix entry (of X d sq).d i j is zero whenever i ≠ j + 1.

Русский

В индуктивно сконструированном ChainComplex с дифференциалами d(n+1) ∘ d(n) = 0, элемент дифференциала d i j равен нулю, если i ≠ j + 1.

LaTeX

$$$ (\\mathrm{of}\\ X\\ d\\ sq).d_{i j} = 0 \\quad\\text{ если } i \\neq j+1$$$

Lean4

theorem of_d_ne {i j : α} (h : i ≠ j + 1) : (of X d sq).d i j = 0 :=
  by
  dsimp [of]
  rw [dif_neg h]

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