multiset_sum_sq — Mathlib

English

For any multiset l of elements in R, the sum of squares equals the square of the sum: l.sum^2 = (l.map (λ x, x^2)).sum.

Русский

Для любого мультимножества l элементов R сумма квадратов равна квадрату суммы: l.sum^2 = сумма квадратов элементов l.

LaTeX

$$$(\\\\operatorname{ringChar}(R) = 2) \\\\Rightarrow (l.sum)^2 = (l.map (\\\\lambda x, x^2)) .sum$$

Lean4

theorem multiset_sum_sq (l : Multiset R) : l.sum ^ 2 = (l.map (· ^ 2)).sum :=
  multiset_sum_pow_char _ _

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