English
Any Pythagorean triple (x,y,z) can be parametrized by integers k,m,n with x,y,z as k(m^2−n^2), k(2mn), k(m^2+n^2) up to order and sign.
Русский
Любой тройка Пифагорa может быть параметризована целыми k,m,n: x,y,z — в виде k(m^2−n^2), k(2mn), k(m^2+n^2) в некотором порядке и знаке.
LaTeX
$$$PythagoreanTriple(x,y,z) \\iff ∃ k,m,n: (x,y,z) = (k(m^2-n^2),k(2mn),k(m^2+n^2))$ или перестановки с знаком.$$
Lean4
/-- By assuming `x` is odd and `z` is positive we get a slightly more precise classification of
the Pythagorean triple `x ^ 2 + y ^ 2 = z ^ 2`. -/
theorem coprime_classification' {x y z : ℤ} (h : PythagoreanTriple x y z) (h_coprime : Int.gcd x y = 1)
(h_parity : x % 2 = 1) (h_pos : 0 < z) :
∃ m n,
x = m ^ 2 - n ^ 2 ∧
y = 2 * m * n ∧ z = m ^ 2 + n ^ 2 ∧ Int.gcd m n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0) ∧ 0 ≤ m :=
by
obtain ⟨m, n, ht1, ht2, ht3, ht4⟩ := PythagoreanTriple.coprime_classification.mp (And.intro h h_coprime)
rcases le_or_gt 0 m with hm | hm
· use m, n
rcases ht1 with h_odd | h_even
· apply And.intro h_odd.1
apply And.intro h_odd.2
rcases ht2 with h_pos | h_neg
· apply And.intro h_pos (And.intro ht3 (And.intro ht4 hm))
· exfalso
revert h_pos
rw [h_neg]
exact imp_false.mpr (not_lt.mpr (neg_nonpos.mpr (by positivity)))
exfalso
rcases h_even with ⟨rfl, -⟩
rw [mul_assoc, Int.mul_emod_right] at h_parity
exact zero_ne_one h_parity
· use -m, -n
rcases ht1 with h_odd | h_even
· rw [neg_sq m]
rw [neg_sq n]
apply And.intro h_odd.1
constructor
· rw [h_odd.2]
ring
rcases ht2 with h_pos | h_neg
· apply And.intro h_pos
constructor
· delta Int.gcd
rw [Int.natAbs_neg, Int.natAbs_neg]
exact ht3
· rw [Int.neg_emod_two, Int.neg_emod_two]
apply And.intro ht4
cutsat
· exfalso
revert h_pos
rw [h_neg]
exact imp_false.mpr (not_lt.mpr (neg_nonpos.mpr (by positivity)))
exfalso
rcases h_even with ⟨rfl, -⟩
rw [mul_assoc, Int.mul_emod_right] at h_parity
exact zero_ne_one h_parity
