English
Let α be a DivisionRing of characteristic zero and s a multiset of rationals. Then the sum of s cast to α equals the sum of the casts of the elements.
Русский
Пусть α — делимое кольцо характеристика ноль и s — мультисет рациональных чисел. Тогда сумма элементов s после приведения к α равна сумме приведённых элементов.
LaTeX
$$$ (\mathrm{sum}\, s)^{\uparrow} = \mathrm{sum}(\mathrm{map}(\uparrow)\, s). $$$
Lean4
@[simp, norm_cast]
theorem cast_multiset_sum (s : Multiset ℚ) : (↑s.sum : α) = (s.map (↑)).sum :=
map_multiset_sum (Rat.castHom α) _