sum_sq — Mathlib

English

For a finite set s and a function f: s → R, (sum over s of f)^2 = sum over s of f^2.

Русский

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

LaTeX

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

Lean4

theorem sum_sq (s : Finset ι) (f : ι → R) : (∑ i ∈ s, f i) ^ 2 = ∑ i ∈ s, f i ^ 2 :=
  sum_pow_char _ _ _

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