English
A primitive Pythagorean triple x,y,z is classified if there exist coprime integers m,n such that either x = m^2 - n^2 and y = 2mn or x = 2mn and y = m^2 - n^2, with gcd(m,n) = 1 and parity condition (m even, n odd) or (m odd, n even).
Русский
Примитивная Пифагорова тройка x,y,z классифицирована, если существуют взаимно простые m,n такие, что либо x = m^2 - n^2 и y = 2mn, либо x = 2mn и y = m^2 - n^2, и gcd(m,n) = 1 с паритетом (m/even, n/odd) или (m/odd, n/even).
LaTeX
$$$\exists m,n \in \mathbb{Z},\;\big(x = m^2 - n^2 \land y = 2mn \lor x = 2mn \land y = m^2 - n^2\big) \land \gcd(m,n) = 1 \land \big((m \equiv 0 \pmod{2} \land n \equiv 1 \pmod{2}) \lor (m \equiv 1 \pmod{2} \land n \equiv 0 \pmod{2})\big)$$$
Lean4
/-- A primitive Pythagorean triple `x, y, z` is a Pythagorean triple with `x` and `y` coprime.
Such a triple is “primitively classified” if there exist coprime integers `m, n` such that either
* `x = m ^ 2 - n ^ 2` and `y = 2 * m * n`, or
* `x = 2 * m * n` and `y = m ^ 2 - n ^ 2`.
-/
@[nolint unusedArguments]
def IsPrimitiveClassified (_ : PythagoreanTriple x y z) :=
∃ m n : ℤ,
(x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n ∨ x = 2 * m * n ∧ y = m ^ 2 - n ^ 2) ∧
Int.gcd m n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0)
