sum_comp — Mathlib

English

Composition distributes over finite sums: (∑ i ∈ s, p_i) ∘ q = ∑ i ∈ s, (p_i ∘ q).

Русский

Композиция распределяется по конечным суммам: (∑ i ∈ s, p_i) ∘ q = ∑ i ∈ s, (p_i ∘ q).

LaTeX

$$$$(\\sum_{i \\in s} p_i).comp q = \\sum_{i \\in s} (p_i.comp q)$$$$

Lean4

@[simp]
theorem sum_comp (s : Finset ι) (p : ι → R[X]) (q : R[X]) : (∑ i ∈ s, p i).comp q = ∑ i ∈ s, (p i).comp q :=
  Polynomial.eval₂_finset_sum _ _ _ _

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