map_list_sum — Mathlib

English

For a RingEquiv f: R ≃+* S and a list l of R, the image of the list product equals the product of the images: f(l.prod) = (l.map f).prod.

Русский

Для кольцевого эквивалента f: R ≃+* S и списка l из R верно: f(l.prod) = (l.map f).prod.

LaTeX

$$$$ f\left(\mathrm{prod}(l)\right) = \mathrm{prod}\left(\mathrm{map}(f,l)\right). $$$$

Lean4

protected theorem map_list_sum [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (f : R ≃+* S) (l : List R) :
    f l.sum = (l.map f).sum :=
  map_list_sum f l

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