headI_add_tail_sum

Mathlib.Algebra.BigOperators.Group.List.Basic

URI: https://scilib.ai/kg/mathlib#List.headI_add_tail_sum

English

For a list of natural numbers, the sum of the tail plus the head equals the total sum.

Русский

Для списка натуральных чисел сумма хвоста плюс первый элемент равна общей сумме списка.

LaTeX

$$L.headI + L.tail.sum = L.sum$$

Lean4

/-- This relies on `default ℕ = 0`. -/
theorem headI_add_tail_sum (L : List ℕ) : L.headI + L.tail.sum = L.sum := by cases L <;> simp

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

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

Разделы

Аффилиация

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