sum_mul_self — Mathlib

English

For a finite set s and f: s → R, (sum f)^2 = sum f^2, i.e., the cross terms vanish in characteristic two.

Русский

Для конечного множества s и функции f: s → R, (сумма f)^2 = сумма f^2, т.е. перекрестные члены исчезают при характеристике две.

LaTeX

$$$(\\\\operatorname{ringChar}(R) = 2) \\\\Rightarrow (\\\\left(\\\\sum i \\\\in s, f(i)\\\\right))^2 = \\\\sum i \\\\in s, f(i)^2$$$

Lean4

theorem sum_mul_self (s : Finset ι) (f : ι → R) : ((∑ i ∈ s, f i) * ∑ i ∈ s, f i) = ∑ i ∈ s, f i * f i := by
  simp_rw [← pow_two, sum_sq]

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