mathlib documentation

number_theory.pythagorean_triples

Pythagorean Triples #

The main result is the classification of Pythagorean triples. The final result is for general Pythagorean triples. It follows from the more interesting relatively prime case. We use the "rational parametrization of the circle" method for the proof. The parametrization maps the point (x / z, y / z) to the slope of the line through (-1 , 0) and (x / z, y / z). This quickly shows that (x / z, y / z) = (2 * m * n / (m ^ 2 + n ^ 2), (m ^ 2 - n ^ 2) / (m ^ 2 + n ^ 2)) where m / n is the slope. In order to identify numerators and denominators we now need results showing that these are coprime. This is easy except for the prime 2. In order to deal with that we have to analyze the parity of x, y, m and n and eliminate all the impossible cases. This takes up the bulk of the proof below.

theorem sq_ne_two_fin_zmod_four (z : zmod 4) :
z * z 2
theorem int.sq_ne_two_mod_four (z : ) :
z * z % 4 2
def pythagorean_triple (x y z : ) :
Prop

Three integers x, y, and z form a Pythagorean triple if x * x + y * y = z * z.

Equations

Pythagorean triples are interchangable, i.e x * x + y * y = y * y + x * x = z * z. This comes from additive commutativity.

The zeroth Pythagorean triple is all zeros.

theorem pythagorean_triple.eq {x y z : } (h : pythagorean_triple x y z) :
x * x + y * y = z * z
@[symm]
theorem pythagorean_triple.symm {x y z : } (h : pythagorean_triple x y z) :
theorem pythagorean_triple.mul {x y z : } (h : pythagorean_triple x y z) (k : ) :
pythagorean_triple (k * x) (k * y) (k * z)

A triple is still a triple if you multiply x, y and z by a constant k.

theorem pythagorean_triple.mul_iff {x y z : } (k : ) (hk : k 0) :
pythagorean_triple (k * x) (k * y) (k * z) pythagorean_triple x y z

(k*x, k*y, k*z) is a Pythagorean triple if and only if (x, y, z) is also a triple.

@[nolint]
def pythagorean_triple.is_classified {x y z : } (h : pythagorean_triple x y z) :
Prop

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).
Equations
@[nolint]

A primitive pythogorean 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.
Equations
theorem pythagorean_triple.even_odd_of_coprime {x y z : } (h : pythagorean_triple x y z) (hc : x.gcd y = 1) :
x % 2 = 0 y % 2 = 1 x % 2 = 1 y % 2 = 0
theorem pythagorean_triple.gcd_dvd {x y z : } (h : pythagorean_triple x y z) :
(x.gcd y) z
theorem pythagorean_triple.normalize {x y z : } (h : pythagorean_triple x y z) :
pythagorean_triple (x / (x.gcd y)) (y / (x.gcd y)) (z / (x.gcd y))
theorem pythagorean_triple.ne_zero_of_coprime {x y z : } (h : pythagorean_triple x y z) (hc : x.gcd y = 1) :
z 0
theorem pythagorean_triple.coprime_of_coprime {x y z : } (h : pythagorean_triple x y z) (hc : x.gcd y = 1) :
y.gcd z = 1

A parametrization of the unit circle #

For the classification of pythogorean triples, we will use a parametrization of the unit circle.

def circle_equiv_gen {K : Type u_1} [field K] (hk : ∀ (x : K), 1 + x ^ 2 0) :
K {p // p.fst ^ 2 + p.snd ^ 2 = 1 p.snd -1}

A parameterization of the unit circle that is useful for classifying Pythagorean triples. (To be applied in the case where K = ℚ.)

Equations
@[simp]
theorem circle_equiv_apply {K : Type u_1} [field K] (hk : ∀ (x : K), 1 + x ^ 2 0) (x : K) :
((circle_equiv_gen hk) x) = (2 * x / (1 + x ^ 2), (1 - x ^ 2) / (1 + x ^ 2))
@[simp]
theorem circle_equiv_symm_apply {K : Type u_1} [field K] (hk : ∀ (x : K), 1 + x ^ 2 0) (v : {p // p.fst ^ 2 + p.snd ^ 2 = 1 p.snd -1}) :
theorem pythagorean_triple.is_primitive_classified_aux {x y z : } (h : pythagorean_triple x y z) (hc : x.gcd y = 1) (hzpos : 0 < z) {m n : } (hm2n2 : 0 < m ^ 2 + n ^ 2) (hv2 : x / z = 2 * m * n / (m ^ 2 + n ^ 2)) (hw2 : y / z = (m ^ 2 - n ^ 2) / (m ^ 2 + n ^ 2)) (H : (m ^ 2 - n ^ 2).gcd (m ^ 2 + n ^ 2) = 1) (co : m.gcd n = 1) (pp : m % 2 = 0 n % 2 = 1 m % 2 = 1 n % 2 = 0) :
theorem pythagorean_triple.is_primitive_classified_of_coprime_of_odd_of_pos {x y z : } (h : pythagorean_triple x y z) (hc : x.gcd y = 1) (hyo : y % 2 = 1) (hzpos : 0 < z) :
theorem pythagorean_triple.coprime_classification {x y z : } :
pythagorean_triple x y z x.gcd 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)) m.gcd n = 1 (m % 2 = 0 n % 2 = 1 m % 2 = 1 n % 2 = 0)
theorem pythagorean_triple.coprime_classification' {x y z : } (h : pythagorean_triple x y z) (h_coprime : x.gcd 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 m.gcd n = 1 (m % 2 = 0 n % 2 = 1 m % 2 = 1 n % 2 = 0) 0 m

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 pythagorean_triple.classification {x y z : } :
pythagorean_triple 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))

Formula for Pythagorean Triples