complex_d_succ_comp — Mathlib

English

The composition of consecutive differentials in the projective resolution is zero: d n (n+1) then d (n+1) (n+2) is zero.

Русский

Состыковка последовательных дифференциалов в разрешении: d n (n+1) затем d (n+1) (n+2) равна нулю.

LaTeX

$$$ P.complex.d\\;n\\; (n+1) \\;\\circ\\; P.complex.d\\;(n+1)\\;(n+2) = 0. $$$

Lean4

theorem complex_d_succ_comp (n : ℕ) : P.complex.d n (n + 1) ≫ P.complex.d (n + 1) (n + 2) = 0 := by simp

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