sum_mul_self_eq_zero_iff — Mathlib

English

Let s be a finite set of indices and f a function from the index set to a linearly ordered ring R. If the sum of the squares f(i)^2 over i in s is zero, then every f(i) with i in s must be zero.

Русский

Пусть s — конечное множество индексов, а f: ι → R. Если сумма квадратов f(i)^2 по i из s равна нулю, то для каждого i ∈ s имеет место f(i) = 0.

LaTeX

$$$\displaystyle \sum_{i \in s} f(i)^2 = 0 \quad\Longleftrightarrow\quad \forall i \in s,\ f(i)=0$$$

Lean4

theorem sum_mul_self_eq_zero_iff [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] [ExistsAddOfLE R] (s : Finset ι)
    (f : ι → R) : ∑ i ∈ s, f i * f i = 0 ↔ ∀ i ∈ s, f i = 0 :=
  by
  rw [sum_eq_zero_iff_of_nonneg fun _ _ ↦ mul_self_nonneg _]
  simp

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