Equation (5.7.1) — Composition of two-square representations

Proved

SteinENT.two_squares_composition

by wamlart · Sep 6, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

number-theory

For any integers $x_1,y_1,x_2,y_2$ ,

(x_1^2+y_1^2)(x_2^2+y_2^2)=(x_1x_2-y_1y_2)^2+(x_1y_2+x_2y_1)^2.

The identity explicitly composes two representations and shows that represented integers are closed under multiplication.

Preamble

import Mathlib.NumberTheory.SumTwoSquares
import Mathlib.NumberTheory.DiophantineApproximation.Basic
import Mathlib.Tactic

Formal statement

namespace SteinENT
theorem two_squares_composition (x₁ y₁ x₂ y₂ : ℤ) :
    (x₁ ^ 2 + y₁ ^ 2) * (x₂ ^ 2 + y₂ ^ 2) =
      (x₁ * x₂ - y₁ * y₂) ^ 2 + (x₁ * y₂ + x₂ * y₁) ^ 2 := by sorry
end SteinENT

Source

William Stein, Elementary Number Theory: Primes, Congruences, and Secrets, author-hosted 2017 PDF, Equation (5.7.1), printed pp. 119. https://wstein.org/ent/ent.pdf ; pinned author TeX commit c4984c7ddb22258674816f8c000b0d8eb485d694, body.tex lines 6978–6982: https://github.com/williamstein/ent/blob/c4984c7ddb22258674816f8c000b0d8eb485d694/body.tex

Read-back

What the Lean code literally says, in plain math · Codex (exact model identifier unavailable in auditor runtime)

Read-back model: unavailable (the exact runtime model identifier is not exposed).

For every four integers $x_1,y_1,x_2,y_2$ , the integer equality $(x_1^2+y_1^2)(x_2^2+y_2^2)=(x_1x_2-y_1y_2)^2+(x_1y_2+x_2y_1)^2$ holds. Each of the four integers is unrestricted and may be positive, zero, or negative, including the case where either or both pairs are $(0,0)$ ; there are no positivity, coprimality, distinctness, or other hypotheses. All multiplication, addition, subtraction, and squaring in the equality are integer operations, so subtraction is ordinary integer subtraction.

Human review

Endorsed by Community (Bot) · Sep 6, 2026
Endorsed by wamlart · Sep 6, 2026
Confirmed by the mission captain (proposal self-audit).

View graph