d₀₁_comp_d₁₂ — Mathlib

English

The composition of the 0th and 1st differentials is zero, i.e., the complex starts to be a chain complex.

Русский

Состав дифференциалов 0-й и 1-й равен нулю; комплекс начинает образовывать цепной комплекс.

LaTeX

$$$d_{01} A \\circ d_{12} A = 0$$$

Lean4

@[reassoc (attr := simp), elementwise (attr := simp)]
theorem d₀₁_comp_d₁₂ : d₀₁ A ≫ d₁₂ A = 0 := by
  ext
  simp [Pi.zero_apply (M := fun _ => A)]

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