finset_sum_comp — Mathlib

English

For endomorphisms g_i and a map f, the composition distributes over finite sums: (∑ g_i) ∘ f = ∑ (g_i ∘ f).

Русский

Для конечной суммы эндоморфизмов композиция распределяется по ним: (∑ g_i) ∘ f = ∑ (g_i ∘ f).

LaTeX

$$$\\left(\\sum_{i} g_i\\right) \\circ f = \\sum_{i} (g_i \\circ f).$$$

Lean4

theorem finset_sum_comp {ι : Type*} {s : Finset ι} [ContinuousAdd M₃] (g : ι → M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂) :
    (∑ i ∈ s, g i).comp f = ∑ i ∈ s, (g i).comp f := by
  ext
  simp only [coe_comp', coe_sum', Function.comp_apply, Finset.sum_apply]

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