English
Let x, y, z be integers with x^2 + y^2 = z^2 and gcd(x, y) = 1. Then there exist integers m, n and a nonzero integer k with gcd(m, n) = 1 and m, n of opposite parity, such that either 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). Conversely, any such triple (with gcd(x, y) = 1) arises from primitive m, n and k.
Русский
Пусть x, y, z — целые числа такие, что x^2 + y^2 = z^2 и gcd(x, y) = 1. Тогда существуют целые m, n и k, причём gcd(m, n) = 1 и m, n имеют противоположную паритетность, такие что либо x = k(m^2 − n^2), y = k(2mn), либо x = k(2mn), y = k(m^2 − n^2), и z = ±k(m^2 + n^2). Обратно, любая примитивная тройка получается таким образом.
LaTeX
$$$ PythagoreanTriple(x,y,z) \land \gcd(x,y)=1 \Longrightarrow \exists k,m,n:\n\quad (x = k(m^2 - n^2) \land y = k(2mn) \lor x = k(2mn) \land y = k(m^2 - n^2)) \land (z = \pm k(m^2 + n^2)) \land \gcd(m,n)=1 \land ((m \mod 2 = 0 \land n \mod 2 = 1) \lor (m \mod 2 = 1 \land n \mod 2 = 0))$$
Lean4
theorem coprime_classification :
PythagoreanTriple x y z ∧ Int.gcd x y = 1 ↔
∃ m n,
(x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n ∨ x = 2 * m * n ∧ y = m ^ 2 - n ^ 2) ∧
(z = m ^ 2 + n ^ 2 ∨ z = -(m ^ 2 + n ^ 2)) ∧
Int.gcd m n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0) :=
by
constructor
· intro h
obtain ⟨m, n, H⟩ := h.left.isPrimitiveClassified_of_coprime h.right
use m, n
rcases H with ⟨⟨rfl, rfl⟩ | ⟨rfl, rfl⟩, co, pp⟩
· refine ⟨Or.inl ⟨rfl, rfl⟩, ?_, co, pp⟩
have : z ^ 2 = (m ^ 2 + n ^ 2) ^ 2 := by
rw [sq, ← h.left.eq]
ring
simpa using eq_or_eq_neg_of_sq_eq_sq _ _ this
· refine ⟨Or.inr ⟨rfl, rfl⟩, ?_, co, pp⟩
have : z ^ 2 = (m ^ 2 + n ^ 2) ^ 2 := by
rw [sq, ← h.left.eq]
ring
simpa using eq_or_eq_neg_of_sq_eq_sq _ _ this
· delta PythagoreanTriple
rintro ⟨m, n, ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩, rfl | rfl, co, pp⟩ <;>
first
| constructor; ring; exact coprime_sq_sub_mul co pp
| constructor; ring; rw [Int.gcd_comm]; exact coprime_sq_sub_mul co pp
