multiset_sum_mul_self — Mathlib

English

For any multiset l of elements in R, l.sum * l.sum = sum of x^2 over l.

Русский

Для любого мультимножества l элементов R: l.sum ⋅ l.sum = сумма x^2 по l.

LaTeX

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

Lean4

theorem multiset_sum_mul_self (l : Multiset R) : l.sum * l.sum = (Multiset.map (fun x => x * x) l).sum := by
  simp_rw [← pow_two, multiset_sum_sq]

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