Documentation

HexConway.Entries.S1_6

source
def Hex.Conway.luebeckConwayPolynomial_113_1 :
FpPoly 113

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

Equations
Instances For
    source
    @[simp]
    theorem Hex.Conway.luebeckConwayPolynomial_113_1_monic :
    DensePoly.Monic luebeckConwayPolynomial_113_1

    Monicity of C(113, 1).

    source
    @[simp]
    theorem Hex.Conway.luebeckConwayPolynomial_113_1_degree_pos :
    0 < luebeckConwayPolynomial_113_1.degree

    Positive degree of C(113, 1).

    source
    @[simp]
    theorem Hex.Conway.luebeckConwayPolynomial?_hit_113_1 :
    luebeckConwayPolynomial? 113 1 = some luebeckConwayPolynomial_113_1

    Lookup identifies the imported C(113, 1).

    source
    def Hex.Conway.luebeckConwayPolynomial_59_1 :
    FpPoly 59

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

    Equations
    Instances For
      source
      @[simp]
      theorem Hex.Conway.luebeckConwayPolynomial_59_1_monic :
      DensePoly.Monic luebeckConwayPolynomial_59_1

      Monicity of C(59, 1).

      source
      @[simp]
      theorem Hex.Conway.luebeckConwayPolynomial_59_1_degree_pos :
      0 < luebeckConwayPolynomial_59_1.degree

      Positive degree of C(59, 1).

      source
      @[simp]
      theorem Hex.Conway.luebeckConwayPolynomial?_hit_59_1 :
      luebeckConwayPolynomial? 59 1 = some luebeckConwayPolynomial_59_1

      Lookup identifies the imported C(59, 1).

      source
      def Hex.Conway.luebeckConwayPolynomial_257_1 :
      FpPoly 257

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

      Equations
      Instances For
        source
        @[simp]
        theorem Hex.Conway.luebeckConwayPolynomial_257_1_monic :
        DensePoly.Monic luebeckConwayPolynomial_257_1

        Monicity of C(257, 1).

        source
        @[simp]
        theorem Hex.Conway.luebeckConwayPolynomial_257_1_degree_pos :
        0 < luebeckConwayPolynomial_257_1.degree

        Positive degree of C(257, 1).

        source
        @[simp]
        theorem Hex.Conway.luebeckConwayPolynomial?_hit_257_1 :
        luebeckConwayPolynomial? 257 1 = some luebeckConwayPolynomial_257_1

        Lookup identifies the imported C(257, 1).

        source
        def Hex.Conway.luebeckConwayPolynomial_13_1 :
        FpPoly 13

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

        Equations
        Instances For
          source
          @[simp]
          theorem Hex.Conway.luebeckConwayPolynomial_13_1_monic :
          DensePoly.Monic luebeckConwayPolynomial_13_1

          Monicity of C(13, 1).

          source
          @[simp]
          theorem Hex.Conway.luebeckConwayPolynomial_13_1_degree_pos :
          0 < luebeckConwayPolynomial_13_1.degree

          Positive degree of C(13, 1).

          source
          @[simp]
          theorem Hex.Conway.luebeckConwayPolynomial?_hit_13_1 :
          luebeckConwayPolynomial? 13 1 = some luebeckConwayPolynomial_13_1

          Lookup identifies the imported C(13, 1).