comp_smul — Mathlib

English

Scalar multiplication in the right argument commutes with composition: z1 ∘ (k • z2) = k • (z1 ∘ z2).

Русский

Умножение на скаляр в правом аргументе commuting с композицией: z1 ∘ (k • z2) = k • (z1 ∘ z2).

LaTeX

$$$\\forall z_1, z_2, k, h,\\ z_1 \\circ (k \\cdot z_2) \\\\; h = k \\cdot (z_1 \\circ z_2) \\\\; h.$$$

Lean4

@[simp]
protected theorem comp_smul {n₁ n₂ n₁₂ : ℤ} (z₁ : Cochain F G n₁) (k : R) (z₂ : Cochain G K n₂) (h : n₁ + n₂ = n₁₂) :
    z₁.comp (k • 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.comp_smul]

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