cast_list_sum — Mathlib

English

Let s be a list of integers and R an AddGroup with one. The cast of the list sum equals the sum of the casts of its elements: (↑s.sum : R) = (s.map (↑)).sum.

Русский

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

LaTeX

$$$\left(\uparrow \sum s_i\right) = \sum (\uparrow s_i)$$$

Lean4

@[simp, norm_cast]
theorem cast_list_sum [AddGroupWithOne R] (s : List ℤ) : (↑s.sum : R) = (s.map (↑)).sum :=
  map_list_sum (castAddHom R) _

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