cast_list_prod — Mathlib

English

Let s be a multiset of integers and R a CommRing. The cast of the product of s equals the product of the casts: (↑s.prod : R) = (s.map (↑)).prod.

Русский

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

LaTeX

$$$\left(\uparrow s.prod\right) = \prod (\uparrow)\, s$$$

Lean4

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

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