cast_list_prod — Mathlib

English

Let R be a semiring and s a finite list of natural numbers. The image of the product of all elements of s in R equals the product of the images of the elements in R. In symbols, (↑(s.prod) : R) = (s.map (↑)).prod.

Русский

Пусть R — полугруппа с единицей, и пусть s — конечный список чисел Нат. Тогда образ произведения всех элементов списка s в R равен произведению образов элементов. Формально: (↑(s.prod) : R) = (s.map (↑)).prod.

LaTeX

$$$\bigl(\uparrow (\prod s)\bigr) = \prod (\uparrow s_i) ,$$$

Lean4

@[simp, norm_cast]
theorem cast_list_prod [Semiring R] (s : List ℕ) : (↑s.prod : R) = (s.map (↑)).prod :=
  map_list_prod (castRingHom R) _

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