English
In an additive commutative monoid with multiplication, if each x_i is a square for i in a finite index set I, then the sum ∑_{i∈I} x_i is a sum of squares.
Русский
В коммутативной аддитивной монойде с умножением, если каждый x_i является квадратом для i в конечном индексе I, то сумма ∑_{i∈I} x_i является суммой квадратов.
LaTeX
$$$\forall \; I: Finset\, \iota, \forall \; x: \iota \to R, \; (\forall i \in I, \operatorname{IsSquare}(x(i))) \Rightarrow \operatorname{IsSumSq}\left(\sum_{i \in I} x(i)\right)$$$
Lean4
/-- In an additive commutative monoid with multiplication,
`∑ i ∈ I, x i`, where each `x i` is a square, is a sum of squares.
-/
theorem sum_isSquare [AddCommMonoid R] [Mul R] {ι : Type*} (I : Finset ι) {x : ι → R} (hx : ∀ i ∈ I, IsSquare <| x i) :
IsSumSq (∑ i ∈ I, x i) := by aesop
