list_sum_mul_self — Mathlib

English

For any finite list l of elements in R, the square of the sum equals the sum of the squares: (sum l)^2 = sum (x^2) over l.

Русский

Для любого конечного списка l из элементов R: (сумма элементов l)^2 = сумма квадратов элементов l.

LaTeX

$$$(\\\\operatorname{ringChar}(R) = 2) \\\\Rightarrow (\\\\left(\\\\sum x \\\\in l, x\\\\right))^2 = \\\\sum x \\\\in l, x^2$$$

Lean4

theorem list_sum_mul_self (l : List R) : l.sum * l.sum = (List.map (fun x => x * x) l).sum := by
  simp_rw [← pow_two, list_sum_sq]

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