cast_multiset_sum — Mathlib

English

Let s be a Finset and f: index → ℤ. The cast of the finite sum equals the finite sum of the casts: ↑(∑ x∈s, f x) = ∑ x∈s, (f x : R).

Русский

Пусть s — множество индексов; f: индексы → ℤ. Образ суммы по s равен сумме образов: ↑(∑ x∈s, f x) = ∑ x∈s, (f x : R).

LaTeX

$$$\uparrow\left(\sum_{x\in s} f(x)\right) = \sum_{x\in s} f(x)^{\uparrow}$$$

Lean4

@[simp, norm_cast]
theorem cast_multiset_sum [AddCommGroupWithOne R] (s : Multiset ℤ) : (↑s.sum : R) = (s.map (↑)).sum :=
  map_multiset_sum (castAddHom R) _

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