English
If a and b are natural numbers expressible as a sum of two squares, then their product ab is also a sum of two squares.
Русский
Если натуральные числа a и b можно записать как суммы двух квадратов, то и произведение ab можно записать как сумму двух квадратов.
LaTeX
$$$ \forall a,b,x,y,u,v \in \mathbb{N},\ (a = x^2 + y^2) \land (b = u^2 + v^2) \rightarrow \exists r,s \in \mathbb{N},\ a b = r^2 + s^2 $$$
Lean4
/-- The set of natural numbers that are sums of two squares is closed under multiplication. -/
theorem sq_add_sq_mul {a b x y u v : ℕ} (ha : a = x ^ 2 + y ^ 2) (hb : b = u ^ 2 + v ^ 2) :
∃ r s : ℕ, a * b = r ^ 2 + s ^ 2 := by
zify at ha hb ⊢
obtain ⟨r, s, h⟩ := _root_.sq_add_sq_mul ha hb
refine ⟨r.natAbs, s.natAbs, ?_⟩
simpa only [Int.natCast_natAbs, sq_abs]
