cast_multiset_sum — Mathlib

English

Let s be a multiset of natural numbers and R a ring with unity. The image of the sum of all elements of s in R equals the sum of their images in R. Symbolically: (↑s.sum : R) = (s.map (↑)).sum.

Русский

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

LaTeX

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

Lean4

@[simp, norm_cast]
theorem cast_multiset_sum [AddCommMonoidWithOne R] (s : Multiset ℕ) : (↑s.sum : R) = (s.map (↑)).sum :=
  map_multiset_sum (castAddMonoidHom R) _

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