map_list_prod — Mathlib

English

Let f be a ring equivalence between nonunital nonassoc semirings. For any list l, the image of the sum equals the sum of the images: f(l.sum) = (l.map f).sum.

Русский

Пусть f — эквивалент кольца между неполными безединичными полусистемами. Для любого списка l выполняется отображение суммы в сумму отображений: f(l.sum) = (l.map f).sum.

LaTeX

$$$$ f\left(\sum l\right) = \sum\left(f(l)\right). $$$$

Lean4

protected theorem map_list_prod [Semiring R] [Semiring S] (f : R ≃+* S) (l : List R) : f l.prod = (l.map f).prod :=
  map_list_prod f l

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