cast_multiset_prod — Mathlib

English

Let s be a multiset of natural numbers and R a commutative semiring. The image of the product of all elements of s in R equals the product of their images in R: (↑s.prod : R) = (s.map (↑)).prod.

Русский

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

LaTeX

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

Lean4

@[simp, norm_cast]
theorem cast_multiset_prod [CommSemiring R] (s : Multiset ℕ) : (↑s.prod : R) = (s.map (↑)).prod :=
  map_multiset_prod (castRingHom R) _

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