English
In a commutative semiring, a finite product of sums of squares is a sum of squares.
Русский
В коммутативной полусистеме конечный произведение сумм квадратов является суммой квадратов.
LaTeX
$$$\forall \; R : \text{ CommSemiring}, \; \forall \iota, \forall I : Finset \iota, \forall x : \iota \to R,\; (\forall i \in I, \operatorname{IsSumSq}(x(i))) \Rightarrow \operatorname{IsSumSq}\left(\prod_{i \in I} x(i)\right)$$$
Lean4
/-- In a commutative semiring, a finite product of sums of squares is a sum of squares. -/
@[aesop unsafe 50% apply]
theorem prod [CommSemiring R] {ι : Type*} {I : Finset ι} {x : ι → R} (hx : ∀ i ∈ I, IsSumSq <| x i) :
IsSumSq (∏ i ∈ I, x i) := by simpa using prod_mem (S := Subsemiring.sumSq R) (by simpa)
