cast_listSum

Mathlib.Data.NNRat.BigOperators

URI: https://scilib.ai/kg/mathlib#NNRat.cast_listSum

English

For any list l of nonnegative rationals, the cast of the sum equals the sum of the casts.

Русский

Для любого списка l из ℚ≥0, привод суммы равен сумме приводов элементов.

LaTeX

$$$(l.sum)^{\uparrow} = (l.map (\uparrow)).sum$$$

Lean4

@[norm_cast]
theorem cast_listSum (l : List ℚ≥0) : (l.sum : K) = (l.map (↑)).sum :=
  map_list_sum (castHom _) _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru