Documentation

LeanPool.PythagoreanPolynomialParametrization.IntegerValued

Integer-valued parametrization of all Pythagorean triples #

This file contains the explicit four-variable integer-valued polynomial triple from Frisch and Vaserstein's main theorem.

source
noncomputable def LeanPool.PythagoreanPolynomialParametrization.xVar :
RatPoly 4

Variable x (index 0) in the 4-variable rational polynomial ring.

Equations
Instances For
    source
    noncomputable def LeanPool.PythagoreanPolynomialParametrization.yVar :
    RatPoly 4

    Variable y (index 1) in the 4-variable rational polynomial ring.

    Equations
    Instances For
      source
      noncomputable def LeanPool.PythagoreanPolynomialParametrization.zVar :
      RatPoly 4

      Variable z (index 2) in the 4-variable rational polynomial ring.

      Equations
      Instances For
        source
        noncomputable def LeanPool.PythagoreanPolynomialParametrization.wVar :
        RatPoly 4

        Variable w (index 3) in the 4-variable rational polynomial ring.

        Equations
        Instances For
          source
          noncomputable def LeanPool.PythagoreanPolynomialParametrization.aParam :
          RatPoly 4

          a = y + z·w

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            noncomputable def LeanPool.PythagoreanPolynomialParametrization.bParam :
            RatPoly 4

            b = z - y·w

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              noncomputable def LeanPool.PythagoreanPolynomialParametrization.cParam :
              RatPoly 4

              c = 2x - x·w

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                noncomputable def LeanPool.PythagoreanPolynomialParametrization.fParam :
                RatPoly 4

                f = c·(a² - b²)/2

                In the paper: ((2x-xw)((y+zw)²-(z-yw)²))/2

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  noncomputable def LeanPool.PythagoreanPolynomialParametrization.gParam :
                  RatPoly 4

                  g = c·a·b

                  In the paper: (2x-xw)(y+zw)(z-yw)

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    noncomputable def LeanPool.PythagoreanPolynomialParametrization.hParam :
                    RatPoly 4

                    h = c·(a² + b²)/2

                    In the paper: ((2x-xw)((y+zw)²+(z-yw)²))/2

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      theorem LeanPool.PythagoreanPolynomialParametrization.f_param_intValued :
                      IsIntValued fParam

                      The first coordinate polynomial in the four-variable parametrization is integer-valued.

                      source
                      theorem LeanPool.PythagoreanPolynomialParametrization.g_param_intValued :
                      IsIntValued gParam

                      The second coordinate polynomial in the four-variable parametrization is integer-valued.

                      source
                      theorem LeanPool.PythagoreanPolynomialParametrization.h_param_intValued :
                      IsIntValued hParam

                      The third coordinate polynomial in the four-variable parametrization is integer-valued.

                      source
                      theorem LeanPool.PythagoreanPolynomialParametrization.exists_int_valued_parametrization :
                      IntValuedParametrizes fParam gParam hParam pythagoreanTriples

                      Frisch--Vaserstein's four-variable integer-valued polynomial parametrization of all Pythagorean triples.