list_sum_sq — Mathlib

English

For any finite list l with 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_sq (l : List R) : l.sum ^ 2 = (l.map (· ^ 2)).sum :=
  list_sum_pow_char _ _

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