comp_zero — Mathlib

English

If you compose a cochain z1 with the zero cochain in degree n2, the result is the zero cochain in degree n12: z1 ∘ (0) = 0.

Русский

Если композиция коцепи z1 с нулевой коцепью даёт нуль в соответствующей степени: z1 ∘ 0 = 0.

LaTeX

$$$\\forall z_1, \\forall h: n_1+n_2=n_{12},\\ z_1 \\circ (0: Cochain G K n_2)\\; h = 0.$$$

Lean4

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

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