cast_multiset_prod — Mathlib

English

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

Русский

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

LaTeX

$$$\left(\uparrow \mathrm{prod}(s)\right) = \mathrm{prod}\left(\uparrow \, s\right)$$$

Lean4

@[simp, norm_cast]
theorem cast_multiset_prod {R : Type*} [CommRing R] (s : Multiset ℤ) : (↑s.prod : R) = (s.map (↑)).prod :=
  map_multiset_prod (castRingHom R) _

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