English
In an additive commutative monoid with multiplication, a finite sum of sums of squares is a sum of squares.
Русский
В коммутативном аддитивном полугруппе с умножением конечная сумма сумм квадратов является суммой квадратов.
LaTeX
$$$\forall \; R, \; [AddCommMonoid\, R] \, [Mul\, R] \, \forall \iota, \forall I : Finset \iota, \forall s : \iota \to R, \, (\forall i \in I, \operatorname{IsSumSq}(s(i))) \Rightarrow \operatorname{IsSumSq}\left(\sum_{i \in I} s(i)\right)$$$
Lean4
/-- In an additive commutative monoid with multiplication, a finite sum of sums of squares
is a sum of squares.
-/
@[aesop unsafe 90% apply]
theorem sum [AddCommMonoid R] [Mul R] {ι : Type*} {I : Finset ι} {s : ι → R} (hs : ∀ i ∈ I, IsSumSq <| s i) :
IsSumSq (∑ i ∈ I, s i) := by simpa using sum_mem (S := AddSubmonoid.sumSq _) hs
