Documentation

HexConway.Entries.S0_6

source
def Hex.Conway.luebeckConwayPolynomial_17_1 :
FpPoly 17

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

Equations
Instances For
    source
    @[simp]
    theorem Hex.Conway.luebeckConwayPolynomial_17_1_monic :
    DensePoly.Monic luebeckConwayPolynomial_17_1

    Monicity of C(17, 1).

    source
    @[simp]
    theorem Hex.Conway.luebeckConwayPolynomial_17_1_degree_pos :
    0 < luebeckConwayPolynomial_17_1.degree

    Positive degree of C(17, 1).

    source
    @[simp]
    theorem Hex.Conway.luebeckConwayPolynomial?_hit_17_1 :
    luebeckConwayPolynomial? 17 1 = some luebeckConwayPolynomial_17_1

    Lookup identifies the imported C(17, 1).

    source
    def Hex.Conway.luebeckConwayPolynomial_5_1 :
    FpPoly 5

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

    Equations
    Instances For
      source
      @[simp]
      theorem Hex.Conway.luebeckConwayPolynomial_5_1_monic :
      DensePoly.Monic luebeckConwayPolynomial_5_1

      Monicity of C(5, 1).

      source
      @[simp]
      theorem Hex.Conway.luebeckConwayPolynomial_5_1_degree_pos :
      0 < luebeckConwayPolynomial_5_1.degree

      Positive degree of C(5, 1).

      source
      @[simp]
      theorem Hex.Conway.luebeckConwayPolynomial?_hit_5_1 :
      luebeckConwayPolynomial? 5 1 = some luebeckConwayPolynomial_5_1

      Lookup identifies the imported C(5, 1).