cast_list_sum — Mathlib

English

If α is a DivisionRing of characteristic zero, then the natural embedding of ℚ into α preserves finite sums over lists: for every list s of rational numbers, the cast of the sum equals the sum of the casts.

Русский

Если α — делимое кольцо с характеристикой ноль, то естественное вложение ℚ в α сохраняет конечную сумму для списков: для любого списка рациональных чисел s верно, что приведение суммы к α равно сумме приведённых элементов.

LaTeX

$$$ \left( \sum s \right)^{\uparrow} = \sum_{i \in s} i^{\uparrow} $$$

Lean4

@[simp, norm_cast]
theorem cast_list_sum (s : List ℚ) : (↑s.sum : α) = (s.map (↑)).sum :=
  map_list_sum (Rat.castHom α) _

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