English
If (x,y,z) is a primitive Pythagorean triple (gcd(x,y)=1, z>0), then there exist integers m,n with gcd(m,n)=1 and a parity condition such that up to sign we have x = m^2 - n^2, y = 2mn, z = m^2 + n^2, with m ≥ 0 and parity constraints.
Русский
Если (x,y,z) — примитивное тройки Пифагора, то существуют m,n целые с gcd(m,n)=1 и заданной парностью, так что (при сохранении знаков) x = m^2 - n^2, y = 2mn, z = m^2 + n^2, и m ≥ 0.
LaTeX
$$$\\exists m,n \\in \\mathbb{Z},\\ x = m^2 - n^2\\;\\land\\; y = 2mn\\;\\land\\; z = m^2 + n^2\\;\\land\\ gcd(m,n)=1\\;\\land\\ (m\\bmod 2 = 0 \\land n\\bmod 2 = 1 \\ \\lor\\ m\\bmod 2 = 1 \\land n\\bmod 2 = 0)\\; \\land\\ 0 \\le m$$$
Lean4
theorem isPrimitiveClassified_aux (hc : x.gcd y = 1) (hzpos : 0 < z) {m n : ℤ} (hm2n2 : 0 < m ^ 2 + n ^ 2)
(hv2 : (x : ℚ) / z = 2 * m * n / ((m : ℚ) ^ 2 + (n : ℚ) ^ 2))
(hw2 : (y : ℚ) / z = ((m : ℚ) ^ 2 - (n : ℚ) ^ 2) / ((m : ℚ) ^ 2 + (n : ℚ) ^ 2))
(H : Int.gcd (m ^ 2 - n ^ 2) (m ^ 2 + n ^ 2) = 1) (co : Int.gcd m n = 1)
(pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0) : h.IsPrimitiveClassified :=
by
have hz : z ≠ 0 := ne_of_gt hzpos
have h2 : y = m ^ 2 - n ^ 2 ∧ z = m ^ 2 + n ^ 2 :=
by
apply Rat.div_int_inj hzpos hm2n2 (h.coprime_of_coprime hc) H
rw [hw2]
norm_cast
use m, n
apply And.intro _ (And.intro co pp)
right
refine ⟨?_, h2.left⟩
rw [← Rat.coe_int_inj _ _, ← div_left_inj' ((mt (Rat.coe_int_inj z 0).mp) hz), hv2, h2.right]
norm_cast
