smul_comp — Mathlib

English

The composition with a zero cochain is zero: (0 : Cochain F G n1).comp z2 h = 0.

Русский

Композиция с нулевым коцепоинтом равна нулю: (0 : Cochain F G n1).comp z2 h = 0.

LaTeX

$$$$ (0: \mathrm{Cochain} F G n_1).\mathrm{comp} z_2 h = 0. $$$$

Lean4

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

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