map_sum — Mathlib

English

Let g be a RingEquiv; for a finite set s and function f: α → R, g (∑_{x∈s} f x) = ∑_{x∈s} g(f x).

Русский

Пусть g — кольцевой эквивалент; для конечного множества s и функции f: α → R выполняется g(∑_{x∈s} f x) = ∑_{x∈s} g(f x).

LaTeX

$$$$ g\left(\sum_{x\in s} f(x)\right) = \sum_{x\in s} g(f(x)). $$$$

Lean4

protected theorem map_sum [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (g : R ≃+* S) (f : α → R)
    (s : Finset α) : g (∑ x ∈ s, f x) = ∑ x ∈ s, g (f x) :=
  map_sum g f s

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