English
Theorem classification: PythagoreanTriple x y z is equivalent to the existence of k,m,n with x = k( m^2−n^2 ) and y = k(2mn) or the swapped form, and z = k(m^2+n^2) or z = −k(m^2+n^2).
Русский
Теорема классификации: PythagoreanTriple x y z эквивалентно существованию k,m,n так, что x = k(m^2−n^2) и y = k(2mn) или наоборот, и z = k(m^2+n^2) или z = −k(m^2+n^2).
LaTeX
$$$PythagoreanTriple(x,y,z) \\iff ∃k,m,n:\\ (x = k(m^2-n^2) \\land y = k(2mn) \\lor x = k(2mn) \\land y = k(m^2-n^2)) \\land (z = k(m^2+n^2) \\lor z = -k(m^2+n^2))$$$
Lean4
/-- **Formula for Pythagorean Triples** -/
theorem classification :
PythagoreanTriple x y z ↔
∃ k m n,
(x = k * (m ^ 2 - n ^ 2) ∧ y = k * (2 * m * n) ∨ x = k * (2 * m * n) ∧ y = k * (m ^ 2 - n ^ 2)) ∧
(z = k * (m ^ 2 + n ^ 2) ∨ z = -k * (m ^ 2 + n ^ 2)) :=
by
constructor
· intro h
obtain ⟨k, m, n, H⟩ := h.classified
use k, m, n
rcases H with (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩)
· refine ⟨Or.inl ⟨rfl, rfl⟩, ?_⟩
have : z ^ 2 = (k * (m ^ 2 + n ^ 2)) ^ 2 := by
rw [sq, ← h.eq]
ring
simpa using eq_or_eq_neg_of_sq_eq_sq _ _ this
· refine ⟨Or.inr ⟨rfl, rfl⟩, ?_⟩
have : z ^ 2 = (k * (m ^ 2 + n ^ 2)) ^ 2 := by
rw [sq, ← h.eq]
ring
simpa using eq_or_eq_neg_of_sq_eq_sq _ _ this
· rintro ⟨k, m, n, ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩, rfl | rfl⟩ <;> delta PythagoreanTriple <;> ring
