Documentation

HexConway.Entries.S3_6

source
def Hex.Conway.luebeckConwayPolynomial_73_1 :
FpPoly 73

Imported C(73, 1), with ascending coefficients.

Equations
Instances For
    source
    @[simp]
    theorem Hex.Conway.luebeckConwayPolynomial_73_1_monic :
    DensePoly.Monic luebeckConwayPolynomial_73_1

    Monicity of C(73, 1).

    source
    @[simp]
    theorem Hex.Conway.luebeckConwayPolynomial_73_1_degree_pos :
    0 < luebeckConwayPolynomial_73_1.degree

    Positive degree of C(73, 1).

    source
    @[simp]
    theorem Hex.Conway.luebeckConwayPolynomial?_hit_73_1 :
    luebeckConwayPolynomial? 73 1 = some luebeckConwayPolynomial_73_1

    Lookup identifies the imported C(73, 1).

    source
    def Hex.Conway.luebeckConwayPolynomial_83_1 :
    FpPoly 83

    Imported C(83, 1), with ascending coefficients.

    Equations
    Instances For
      source
      @[simp]
      theorem Hex.Conway.luebeckConwayPolynomial_83_1_monic :
      DensePoly.Monic luebeckConwayPolynomial_83_1

      Monicity of C(83, 1).

      source
      @[simp]
      theorem Hex.Conway.luebeckConwayPolynomial_83_1_degree_pos :
      0 < luebeckConwayPolynomial_83_1.degree

      Positive degree of C(83, 1).

      source
      @[simp]
      theorem Hex.Conway.luebeckConwayPolynomial?_hit_83_1 :
      luebeckConwayPolynomial? 83 1 = some luebeckConwayPolynomial_83_1

      Lookup identifies the imported C(83, 1).

      source
      def Hex.Conway.luebeckConwayPolynomial_107_1 :
      FpPoly 107

      Imported C(107, 1), with ascending coefficients.

      Equations
      Instances For
        source
        @[simp]
        theorem Hex.Conway.luebeckConwayPolynomial_107_1_monic :
        DensePoly.Monic luebeckConwayPolynomial_107_1

        Monicity of C(107, 1).

        source
        @[simp]
        theorem Hex.Conway.luebeckConwayPolynomial_107_1_degree_pos :
        0 < luebeckConwayPolynomial_107_1.degree

        Positive degree of C(107, 1).

        source
        @[simp]
        theorem Hex.Conway.luebeckConwayPolynomial?_hit_107_1 :
        luebeckConwayPolynomial? 107 1 = some luebeckConwayPolynomial_107_1

        Lookup identifies the imported C(107, 1).

        source
        def Hex.Conway.luebeckConwayPolynomial_47_1 :
        FpPoly 47

        Imported C(47, 1), with ascending coefficients.

        Equations
        Instances For
          source
          @[simp]
          theorem Hex.Conway.luebeckConwayPolynomial_47_1_monic :
          DensePoly.Monic luebeckConwayPolynomial_47_1

          Monicity of C(47, 1).

          source
          @[simp]
          theorem Hex.Conway.luebeckConwayPolynomial_47_1_degree_pos :
          0 < luebeckConwayPolynomial_47_1.degree

          Positive degree of C(47, 1).

          source
          @[simp]
          theorem Hex.Conway.luebeckConwayPolynomial?_hit_47_1 :
          luebeckConwayPolynomial? 47 1 = some luebeckConwayPolynomial_47_1

          Lookup identifies the imported C(47, 1).

          source
          def Hex.Conway.luebeckConwayPolynomial_23_1 :
          FpPoly 23

          Imported C(23, 1), with ascending coefficients.

          Equations
          Instances For
            source
            @[simp]
            theorem Hex.Conway.luebeckConwayPolynomial_23_1_monic :
            DensePoly.Monic luebeckConwayPolynomial_23_1

            Monicity of C(23, 1).

            source
            @[simp]
            theorem Hex.Conway.luebeckConwayPolynomial_23_1_degree_pos :
            0 < luebeckConwayPolynomial_23_1.degree

            Positive degree of C(23, 1).

            source
            @[simp]
            theorem Hex.Conway.luebeckConwayPolynomial?_hit_23_1 :
            luebeckConwayPolynomial? 23 1 = some luebeckConwayPolynomial_23_1

            Lookup identifies the imported C(23, 1).

            source
            def Hex.Conway.luebeckConwayPolynomial_7_1 :
            FpPoly 7

            Imported C(7, 1), with ascending coefficients.

            Equations
            Instances For
              source
              @[simp]
              theorem Hex.Conway.luebeckConwayPolynomial_7_1_monic :
              DensePoly.Monic luebeckConwayPolynomial_7_1

              Monicity of C(7, 1).

              source
              @[simp]
              theorem Hex.Conway.luebeckConwayPolynomial_7_1_degree_pos :
              0 < luebeckConwayPolynomial_7_1.degree

              Positive degree of C(7, 1).

              source
              @[simp]
              theorem Hex.Conway.luebeckConwayPolynomial?_hit_7_1 :
              luebeckConwayPolynomial? 7 1 = some luebeckConwayPolynomial_7_1

              Lookup identifies the imported C(7, 1).

              source
              def Hex.Conway.luebeckConwayPolynomial_3_1 :
              FpPoly 3

              Imported C(3, 1), with ascending coefficients.

              Equations
              Instances For
                source
                @[simp]
                theorem Hex.Conway.luebeckConwayPolynomial_3_1_monic :
                DensePoly.Monic luebeckConwayPolynomial_3_1

                Monicity of C(3, 1).

                source
                @[simp]
                theorem Hex.Conway.luebeckConwayPolynomial_3_1_degree_pos :
                0 < luebeckConwayPolynomial_3_1.degree

                Positive degree of C(3, 1).

                source
                @[simp]
                theorem Hex.Conway.luebeckConwayPolynomial?_hit_3_1 :
                luebeckConwayPolynomial? 3 1 = some luebeckConwayPolynomial_3_1

                Lookup identifies the imported C(3, 1).