English
A Pythagorean triple is classified if there exist integers k, m, n with either x = k(m^2 - n^2) and y = 2kmn or x = 2kmn and y = k(m^2 - n^2), and gcd(m,n) = 1.
Русский
Пифагова тройка классифицирована, если существуют целые k, m, n такие, что либо x = k(m^2 - n^2) и y = 2kmn, либо x = 2kmn и y = k(m^2 - n^2), и gcd(m,n) = 1.
LaTeX
$$$\exists k,m,n \in \mathbb{Z},\;\big(x = k(m^2 - n^2) \land y = 2kmn \lor x = 2kmn \land y = k(m^2 - n^2)\big) \land \gcd(m,n) = 1$$$
Lean4
/-- A Pythagorean triple `x, y, z` is “classified” if there exist integers `k, m, n` such that
either
* `x = k * (m ^ 2 - n ^ 2)` and `y = k * (2 * m * n)`, or
* `x = k * (2 * m * n)` and `y = k * (m ^ 2 - n ^ 2)`. -/
@[nolint unusedArguments]
def IsClassified (_ : 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)) ∧ Int.gcd m n = 1
