English
In any commutative ring, the set of sums of two squares is closed under multiplication: if a = x^2 + y^2 and b = u^2 + v^2, then ab = r^2 + s^2 with r = xu − yv and s = xv + yu.
Русский
В любом коммутативном кольце множество сумм двух квадратов замкнуно относительно умножения: если a = x^2 + y^2 и b = u^2 + v^2, то ab = r^2 + s^2 с r = xu − yv и s = xv + yu.
LaTeX
$$$\exists r,s \in R,\ a b = r^2 + s^2 \\text{where } a = x^2 + y^2,\ b = u^2 + v^2,\ r = x u - y v,\ s = x v + y u$$$
Lean4
/-- The set of sums of two squares is closed under multiplication in any commutative ring.
See also `sq_add_sq_mul_sq_add_sq`. -/
theorem sq_add_sq_mul {R} [CommRing R] {a b x y u v : R} (ha : a = x ^ 2 + y ^ 2) (hb : b = u ^ 2 + v ^ 2) :
∃ r s : R, a * b = r ^ 2 + s ^ 2 :=
⟨x * u - y * v, x * v + y * u, by rw [ha, hb]; ring⟩
