Documentation

Mathlib.NumberTheory.PythagoreanTriples

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 PythagoreanTriple (x : ) (y : ) (z : ) :

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

Equations
Instances For

    Pythagorean triples are interchangeable, 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 PythagoreanTriple.eq {x : } {y : } {z : } (h : PythagoreanTriple x y z) :
    x * x + y * y = z * z
    theorem PythagoreanTriple.symm {x : } {y : } {z : } (h : PythagoreanTriple x y z) :
    theorem PythagoreanTriple.mul {x : } {y : } {z : } (h : PythagoreanTriple x y z) (k : ) :
    PythagoreanTriple (k * x) (k * y) (k * z)

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

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

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

    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
    Instances For

      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.
      Equations
      Instances For
        theorem PythagoreanTriple.mul_isClassified {x : } {y : } {z : } (h : PythagoreanTriple x y z) (k : ) (hc : h.IsClassified) :
        .IsClassified
        theorem PythagoreanTriple.even_odd_of_coprime {x : } {y : } {z : } (h : PythagoreanTriple x y z) (hc : x.gcd y = 1) :
        x % 2 = 0 y % 2 = 1 x % 2 = 1 y % 2 = 0
        theorem PythagoreanTriple.gcd_dvd {x : } {y : } {z : } (h : PythagoreanTriple x y z) :
        (x.gcd y) z
        theorem PythagoreanTriple.normalize {x : } {y : } {z : } (h : PythagoreanTriple x y z) :
        PythagoreanTriple (x / (x.gcd y)) (y / (x.gcd y)) (z / (x.gcd y))
        theorem PythagoreanTriple.isClassified_of_isPrimitiveClassified {x : } {y : } {z : } (h : PythagoreanTriple x y z) (hp : h.IsPrimitiveClassified) :
        h.IsClassified
        theorem PythagoreanTriple.isClassified_of_normalize_isPrimitiveClassified {x : } {y : } {z : } (h : PythagoreanTriple x y z) (hc : .IsPrimitiveClassified) :
        h.IsClassified
        theorem PythagoreanTriple.ne_zero_of_coprime {x : } {y : } {z : } (h : PythagoreanTriple x y z) (hc : x.gcd y = 1) :
        z 0
        theorem PythagoreanTriple.isPrimitiveClassified_of_coprime_of_zero_left {x : } {y : } {z : } (h : PythagoreanTriple x y z) (hc : x.gcd y = 1) (hx : x = 0) :
        h.IsPrimitiveClassified
        theorem PythagoreanTriple.coprime_of_coprime {x : } {y : } {z : } (h : PythagoreanTriple x y z) (hc : x.gcd y = 1) :
        y.gcd z = 1

        A parametrization of the unit circle #

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

        def circleEquivGen {K : Type u_1} [Field K] (hk : ∀ (x : K), 1 + x ^ 2 0) :
        K { p : K × K // p.1 ^ 2 + p.2 ^ 2 = 1 p.2 -1 }

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

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[simp]
          theorem circleEquivGen_apply {K : Type u_1} [Field K] (hk : ∀ (x : K), 1 + x ^ 2 0) (x : K) :
          ((circleEquivGen hk) x) = (2 * x / (1 + x ^ 2), (1 - x ^ 2) / (1 + x ^ 2))
          @[simp]
          theorem circleEquivGen_symm_apply {K : Type u_1} [Field K] (hk : ∀ (x : K), 1 + x ^ 2 0) (v : { p : K × K // p.1 ^ 2 + p.2 ^ 2 = 1 p.2 -1 }) :
          (circleEquivGen hk).symm v = (↑v).1 / ((↑v).2 + 1)
          theorem PythagoreanTriple.isPrimitiveClassified_aux {x : } {y : } {z : } (h : PythagoreanTriple 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.IsPrimitiveClassified
          theorem PythagoreanTriple.isPrimitiveClassified_of_coprime_of_odd_of_pos {x : } {y : } {z : } (h : PythagoreanTriple x y z) (hc : x.gcd y = 1) (hyo : y % 2 = 1) (hzpos : 0 < z) :
          h.IsPrimitiveClassified
          theorem PythagoreanTriple.isPrimitiveClassified_of_coprime_of_pos {x : } {y : } {z : } (h : PythagoreanTriple x y z) (hc : x.gcd y = 1) (hzpos : 0 < z) :
          h.IsPrimitiveClassified
          theorem PythagoreanTriple.isPrimitiveClassified_of_coprime {x : } {y : } {z : } (h : PythagoreanTriple x y z) (hc : x.gcd y = 1) :
          h.IsPrimitiveClassified
          theorem PythagoreanTriple.classified {x : } {y : } {z : } (h : PythagoreanTriple x y z) :
          h.IsClassified
          theorem PythagoreanTriple.coprime_classification {x : } {y : } {z : } :
          PythagoreanTriple 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 PythagoreanTriple.coprime_classification' {x : } {y : } {z : } (h : PythagoreanTriple 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 PythagoreanTriple.classification {x : } {y : } {z : } :
          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))

          Formula for Pythagorean Triples