comp_assoc_of_third_is_zero_cochain

English

If z3 is a zero cochain of degree 0, associativity reduces similarly to the previous case.

Русский

Если z3 — нулевой коцепоинт степени 0, ассоциативность аналогична предыдущему случаю.

LaTeX

$$$$ (z_1.comp z_2 h_{12}).comp z_3 h_{13} = z_1.comp (z_2.comp z_3 (zero\_add n_3)) h_{12}. $$$$

Lean4

@[simp]
theorem comp_assoc_of_third_is_zero_cochain {n₁ n₂ n₁₂ : ℤ} (z₁ : Cochain F G n₁) (z₂ : Cochain G K n₂)
    (z₃ : Cochain K L 0) (h₁₂ : n₁ + n₂ = n₁₂) :
    (z₁.comp z₂ h₁₂).comp z₃ (add_zero n₁₂) = z₁.comp (z₂.comp z₃ (add_zero n₂)) h₁₂ :=
  comp_assoc _ _ _ _ _ (by cutsat)

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