cast_multiset_sum — Mathlib

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 α) _

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