cochainComplex_d_succ_succ_zero — Mathlib

English

In any cochain complex, the differential from degree 0 to degree i+2 is zero for every i.

Русский

В любом когомологическом комплексе дифференциал от степени 0 к степени i+2 равен нулю для всякого i.

LaTeX

$$$d^0_{\,i+2} = 0 \quad \\text{for all } i \\in \\mathbb{N}$$$

Lean4

@[simp]
theorem cochainComplex_d_succ_succ_zero (C : CochainComplex V ℕ) (i : ℕ) : C.d 0 (i + 2) = 0 :=
  by
  rw [C.shape]
  simp only [ComplexShape.up_Rel, zero_add]
  exact (Nat.one_lt_succ_succ _).ne

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