Documentation

HexConway.Entries.S2_6

source
def Hex.Conway.luebeckConwayPolynomial_37_1 :
FpPoly 37

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

Equations
Instances For
    source
    @[simp]
    theorem Hex.Conway.luebeckConwayPolynomial_37_1_monic :
    DensePoly.Monic luebeckConwayPolynomial_37_1

    Monicity of C(37, 1).

    source
    @[simp]
    theorem Hex.Conway.luebeckConwayPolynomial_37_1_degree_pos :
    0 < luebeckConwayPolynomial_37_1.degree

    Positive degree of C(37, 1).

    source
    @[simp]
    theorem Hex.Conway.luebeckConwayPolynomial?_hit_37_1 :
    luebeckConwayPolynomial? 37 1 = some luebeckConwayPolynomial_37_1

    Lookup identifies the imported C(37, 1).

    source
    def Hex.Conway.luebeckConwayPolynomial_41_1 :
    FpPoly 41

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

    Equations
    Instances For
      source
      @[simp]
      theorem Hex.Conway.luebeckConwayPolynomial_41_1_monic :
      DensePoly.Monic luebeckConwayPolynomial_41_1

      Monicity of C(41, 1).

      source
      @[simp]
      theorem Hex.Conway.luebeckConwayPolynomial_41_1_degree_pos :
      0 < luebeckConwayPolynomial_41_1.degree

      Positive degree of C(41, 1).

      source
      @[simp]
      theorem Hex.Conway.luebeckConwayPolynomial?_hit_41_1 :
      luebeckConwayPolynomial? 41 1 = some luebeckConwayPolynomial_41_1

      Lookup identifies the imported C(41, 1).

      source
      def Hex.Conway.luebeckConwayPolynomial_19_1 :
      FpPoly 19

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

      Equations
      Instances For
        source
        @[simp]
        theorem Hex.Conway.luebeckConwayPolynomial_19_1_monic :
        DensePoly.Monic luebeckConwayPolynomial_19_1

        Monicity of C(19, 1).

        source
        @[simp]
        theorem Hex.Conway.luebeckConwayPolynomial_19_1_degree_pos :
        0 < luebeckConwayPolynomial_19_1.degree

        Positive degree of C(19, 1).

        source
        @[simp]
        theorem Hex.Conway.luebeckConwayPolynomial?_hit_19_1 :
        luebeckConwayPolynomial? 19 1 = some luebeckConwayPolynomial_19_1

        Lookup identifies the imported C(19, 1).

        source
        def Hex.Conway.luebeckConwayPolynomial_11_1 :
        FpPoly 11

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

        Equations
        Instances For
          source
          @[simp]
          theorem Hex.Conway.luebeckConwayPolynomial_11_1_monic :
          DensePoly.Monic luebeckConwayPolynomial_11_1

          Monicity of C(11, 1).

          source
          @[simp]
          theorem Hex.Conway.luebeckConwayPolynomial_11_1_degree_pos :
          0 < luebeckConwayPolynomial_11_1.degree

          Positive degree of C(11, 1).

          source
          @[simp]
          theorem Hex.Conway.luebeckConwayPolynomial?_hit_11_1 :
          luebeckConwayPolynomial? 11 1 = some luebeckConwayPolynomial_11_1

          Lookup identifies the imported C(11, 1).

          source
          def Hex.Conway.luebeckConwayPolynomial_2_1 :
          FpPoly 2

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

          Equations
          Instances For
            source
            @[simp]
            theorem Hex.Conway.luebeckConwayPolynomial_2_1_monic :
            DensePoly.Monic luebeckConwayPolynomial_2_1

            Monicity of C(2, 1).

            source
            @[simp]
            theorem Hex.Conway.luebeckConwayPolynomial_2_1_degree_pos :
            0 < luebeckConwayPolynomial_2_1.degree

            Positive degree of C(2, 1).

            source
            @[simp]
            theorem Hex.Conway.luebeckConwayPolynomial?_hit_2_1 :
            luebeckConwayPolynomial? 2 1 = some luebeckConwayPolynomial_2_1

            Lookup identifies the imported C(2, 1).