English
If s1 and s2 are sums of squares in a commutative semiring, then their product s1 · s2 is also a sum of squares.
Русский
Если s1 и s2 являются суммами квадратов, то их произведение s1 · s2 тоже является суммой квадратов.
LaTeX
$$$\forall \; s_1,s_2,\; IsSumSq(s_1) \to IsSumSq(s_2) \to IsSumSq(s_1 \cdot s_2)$$$
Lean4
/-- In a commutative (possibly non-unital) semiring,
if `s₁` and `s₂` are sums of squares, then `s₁ * s₂` is a sum of squares.
-/
@[aesop unsafe 90% apply]
theorem mul [NonUnitalCommSemiring R] {s₁ s₂ : R} (h₁ : IsSumSq s₁) (h₂ : IsSumSq s₂) : IsSumSq (s₁ * s₂) := by
simpa using mul_mem (by simpa : _ ∈ NonUnitalSubsemiring.sumSq R) (by simpa)
