comp_zero — Mathlib

English

Composition distributes over finite sums: for g_i endomorphisms and f, the composition with the sum equals the sum of compositions.

Русский

Композиция распределяет сумму по конечному числу индексов: g_i ◦ f суммируется по i как сумма композиций.

LaTeX

$$$\\big(\\sum_{i\\in s} g_i\\big) \\circ f = \\sum_{i\\in s} (g_i \\circ f).$$$

Lean4

@[simp]
theorem comp_zero (g : M₂ →SL[σ₂₃] M₃) : g.comp (0 : M₁ →SL[σ₁₂] M₂) = 0 :=
  by
  ext
  simp

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