map_sum — Mathlib

English

A continuous algebra homomorphism preserves finite sums: it distributes over finite sums of its arguments.

Русский

Непрерывный алгеброгомоморфизм сохраняет конечные суммы: он распадается по суммам конечного числа слагаемых.

LaTeX

$$$f\\Bigl(\\sum_{i\\in s} g(i)\\Bigr) = \\sum_{i\\in s} f(g(i)).$$$

Lean4

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

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