map_sum — Mathlib

English

Polynomial.map distributes over finite sums: map f of a Finset sum equals the Finset sum of maps.

Русский

Полином-map распределяется по конечной сумме: map f от суммы равен сумме отображений.

LaTeX

$$$$ \\mathrm{map} f \\big(\\sum i \\in s, g_i\\big) = \\sum i \\in s, \\mathrm{map} f (g_i) $$$$

Lean4

protected theorem map_sum {ι : Type*} (g : ι → R[X]) (s : Finset ι) : (∑ i ∈ s, g i).map f = ∑ i ∈ s, (g i).map f :=
  map_sum (mapRingHom f) _ _

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