cast_list_sum — Mathlib

English

simp-lemma for Nat.cast of sums in lists: the cast of a sum of naturals equals the sum of the casts.

Русский

simp-лемма для приведения сумм списков чисел Нат: приведение суммы равно сумме приведений.

LaTeX

$$$\\text{[simp]}\\ (\\sum i\\in s, (i: R)) = \\left(\\sum i\\in s, i\\right)^{\\text{cast}}$$$

Lean4

@[simp, norm_cast]
theorem cast_list_sum [AddMonoidWithOne R] (s : List ℕ) : (↑s.sum : R) = (s.map (↑)).sum :=
  map_list_sum (castAddMonoidHom R) _

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