sub_comp — Mathlib

English

Associativity of cochain composition in full generality: (z1.comp z2 h12).comp z3 h23 equals z1.comp (z2.comp z3 h23) with the appropriate combined degree equation.

Русский

Обобщенная ассоциативность композиции коцепоинтов: (z1.comp z2 h12).comp z3 h23 = z1.comp (z2.comp z3 h23) при соответствующем сочетании степеней.

LaTeX

$$$$ (z_1.comp z_2 h_{12}).comp z_3 h_{23} = z_1.comp (z_2.comp z_3 h_{23}) (h_{12,23}). $$$$

Lean4

@[simp]
protected theorem sub_comp {n₁ n₂ n₁₂ : ℤ} (z₁ z₁' : Cochain F G n₁) (z₂ : Cochain G K n₂) (h : n₁ + n₂ = n₁₂) :
    (z₁ - z₁').comp z₂ h = z₁.comp z₂ h - z₁'.comp z₂ h :=
  by
  ext p q hpq
  simp only [comp_v _ _ h p _ q rfl (by cutsat), sub_v, sub_comp]

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