sum_mul_self — Mathlib

English

In an additive commutative monoid with multiplication, the sum ∑_{i∈I} a_i · a_i is a sum of squares.

Русский

В коммутативной аддитивной моноиде с умножением сумма $\sum_{i∈I} a_i \cdot a_i$ является суммой квадратов.

LaTeX

$$$\operatorname{IsSumSq}\left(\sum_{i \in I} a(i) \cdot a(i)\right)$$$

Lean4

/-- In an additive commutative monoid with multiplication,
`∑ i ∈ I, a i * a i` is a sum of squares.
-/
@[simp↓]
theorem sum_mul_self [AddCommMonoid R] [Mul R] {ι : Type*} (I : Finset ι) (a : ι → R) : IsSumSq (∑ i ∈ I, a i * a i) :=
  by aesop

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