mathlib3 documentation

number_theory.pythagorean_triples

Pythagorean Triples #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

source
theorem sq_ne_two_fin_zmod_four (z : zmod 4) :
z * z ≠ 2
source
theorem int.sq_ne_two_mod_four (z : ℤ) :
z * z % 4 ≠ 2
source
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
source
theorem pythagorean_triple_comm {x y z : ℤ} :
pythagorean_triple x y z ↔ pythagorean_triple y x z

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

source
theorem pythagorean_triple.zero  :
pythagorean_triple 0 0 0

The zeroth Pythagorean triple is all zeros.

source
theorem pythagorean_triple.eq {x y z : ℤ} (h : pythagorean_triple x y z) :
x * x + y * y = z * z
source
@[symm]
theorem pythagorean_triple.symm {x y z : ℤ} (h : pythagorean_triple x y z) :
pythagorean_triple y x z
source
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.

source
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.

source
@[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
source
@[nolint]
def pythagorean_triple.is_primitive_classified {x y z : ℤ} (h : pythagorean_triple x y z) :
Prop

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
source
theorem pythagorean_triple.mul_is_classified {x y z : ℤ} (h : pythagorean_triple x y z) (k : ℤ) (hc : h.is_classified) :
_.is_classified
source
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
source
theorem pythagorean_triple.gcd_dvd {x y z : ℤ} (h : pythagorean_triple x y z) :
↑(x.gcd y) ∣ z
source
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))
source
theorem pythagorean_triple.is_classified_of_is_primitive_classified {x y z : ℤ} (h : pythagorean_triple x y z) (hp : h.is_primitive_classified) :
h.is_classified
source
theorem pythagorean_triple.is_classified_of_normalize_is_primitive_classified {x y z : ℤ} (h : pythagorean_triple x y z) (hc : _.is_primitive_classified) :
h.is_classified
source
theorem pythagorean_triple.ne_zero_of_coprime {x y z : ℤ} (h : pythagorean_triple x y z) (hc : x.gcd y = 1) :
z ≠ 0
source
theorem pythagorean_triple.is_primitive_classified_of_coprime_of_zero_left {x y z : ℤ} (h : pythagorean_triple x y z) (hc : x.gcd y = 1) (hx : x = 0) :
h.is_primitive_classified
source
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.

source
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
source
@[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))
source
@[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}) :
⇑((circle_equiv_gen hk).symm) v = ↑v.fst / (↑v.snd + 1)
source
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) :
h.is_primitive_classified
source
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) :
h.is_primitive_classified
source
theorem pythagorean_triple.is_primitive_classified_of_coprime_of_pos {x y z : ℤ} (h : pythagorean_triple x y z) (hc : x.gcd y = 1) (hzpos : 0 < z) :
h.is_primitive_classified
source
theorem pythagorean_triple.is_primitive_classified_of_coprime {x y z : ℤ} (h : pythagorean_triple x y z) (hc : x.gcd y = 1) :
h.is_primitive_classified
source
theorem pythagorean_triple.classified {x y z : ℤ} (h : pythagorean_triple x y z) :
h.is_classified
source
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)
source
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

source
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