English
Let x, y, z be integers with x^2 + y^2 = z^2. Then either the triple is degenerate (the standard degenerate case) or there exist integers m, n and a nonzero integer k such that the triple is obtained from the classical parametrization: x = k(m^2 − n^2), y = k(2mn) or x = k(2mn), y = k(m^2 − n^2), and z = ±k(m^2 + n^2). In addition, gcd(m, n) = 1 and m and n have opposite parity (one even, one odd). Conversely, any choice of k, m, n with these conditions yields a Pythagorean triple.
Русский
Пусть x, y, z — целые числа such that x^2 + y^2 = z^2. Тогда либо тройка вырождена (обычный вырожденный случай), либо существуют целые m, n и не нуль q такой, что тройка получается из классической параметризации: x = q(m^2 − n^2), y = q(2mn) или x = q(2mn), y = q(m^2 − n^2), и z = ±q(m^2 + n^2). При этом gcd(m, n) = 1 и m и n имеют противоположную четность (один четный, другой нечетный). Обратно, любые такие m, n, q дают Пифагорову тройку.
LaTeX
$$$ x^2 + y^2 = z^2 \quad \Longleftrightarrow \quad \exists k\in\mathbb{Z}_{\neq 0}, \exists m,n\in\mathbb{Z} :
\begin{cases} (x = k(m^2 - n^2) \wedge y = k(2mn)) \lor (x = k(2mn) \wedge y = k(m^2 - n^2)), \\ z = k(m^2 + n^2) \quad \text{or} \quad z = -k(m^2 + n^2), \\ \gcd(m,n) = 1, \ (m \text{ even} \wedge n \text{ odd}) \lor (m \text{ odd} \wedge n \text{ even}) \end{cases}$$
Lean4
theorem classified : h.IsClassified := by
by_cases h0 : Int.gcd x y = 0
· have hx : x = 0 := by
apply Int.natAbs_eq_zero.mp
apply Nat.eq_zero_of_gcd_eq_zero_left h0
have hy : y = 0 := by
apply Int.natAbs_eq_zero.mp
apply Nat.eq_zero_of_gcd_eq_zero_right h0
use 0, 1, 0
simp [hx, hy]
apply h.isClassified_of_normalize_isPrimitiveClassified
apply h.normalize.isPrimitiveClassified_of_coprime
apply Int.gcd_div_gcd_div_gcd (Nat.pos_of_ne_zero h0)
