sum_comp — Mathlib

English

Similarly, the sum of compositions distributes: (∑i α_i) ∘ β = ∑i (α_i ∘ β) for appropriate α_i and β.

Русский

Аналогично, сумма композиций распределяется: (∑i α_i) ∘ β = ∑i (α_i ∘ β).

LaTeX

$$$\big(\sum_i \alpha_i\big).comp\beta = \sum_i (\alpha_i.\comp\beta)$$$

Lean4

theorem sum_comp {X Y Z : C} {p : ℕ} {ι : Type*} [Fintype ι] (α : ι → Ext X Y p) {q : ℕ} (β : Ext Y Z q) {n : ℕ}
    (h : p + q = n) : (∑ i, α i).comp β h = ∑ i, (α i).comp β h :=
  map_sum (β.postcomp X h) _ _

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