def Hex.Conway.luebeckConwayPolynomial_421_2 : FpPoly 421

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

Equations

• Hex.Conway.luebeckConwayPolynomial_421_2 = { coeffs := #[2, 417, 1], normalized := Hex.Conway.luebeckConwayPolynomial_421_2._proof_1 }

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_421_2_monic : DensePoly.Monic luebeckConwayPolynomial_421_2

Monicity of C(421, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_421_2_degree_pos : 0 < luebeckConwayPolynomial_421_2.degree

Positive degree of C(421, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_421_2 : luebeckConwayPolynomial? 421 2 = some luebeckConwayPolynomial_421_2

Lookup identifies the imported C(421, 2).

def Hex.Conway.luebeckConwayPolynomial_491_2 : FpPoly 491

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

Equations

• Hex.Conway.luebeckConwayPolynomial_491_2 = { coeffs := #[2, 487, 1], normalized := Hex.Conway.luebeckConwayPolynomial_491_2._proof_1 }

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_491_2_monic : DensePoly.Monic luebeckConwayPolynomial_491_2

Monicity of C(491, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_491_2_degree_pos : 0 < luebeckConwayPolynomial_491_2.degree

Positive degree of C(491, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_491_2 : luebeckConwayPolynomial? 491 2 = some luebeckConwayPolynomial_491_2

Lookup identifies the imported C(491, 2).

def Hex.Conway.luebeckConwayPolynomial_139_2 : FpPoly 139

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

Equations

• Hex.Conway.luebeckConwayPolynomial_139_2 = { coeffs := #[2, 138, 1], normalized := Hex.Conway.luebeckConwayPolynomial_139_2._proof_1 }

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_139_2_monic : DensePoly.Monic luebeckConwayPolynomial_139_2

Monicity of C(139, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_139_2_degree_pos : 0 < luebeckConwayPolynomial_139_2.degree

Positive degree of C(139, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_139_2 : luebeckConwayPolynomial? 139 2 = some luebeckConwayPolynomial_139_2

Lookup identifies the imported C(139, 2).

def Hex.Conway.luebeckConwayPolynomial_229_2 : FpPoly 229

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

Equations

• Hex.Conway.luebeckConwayPolynomial_229_2 = { coeffs := #[6, 228, 1], normalized := Hex.Conway.luebeckConwayPolynomial_229_2._proof_1 }

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_229_2_monic : DensePoly.Monic luebeckConwayPolynomial_229_2

Monicity of C(229, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_229_2_degree_pos : 0 < luebeckConwayPolynomial_229_2.degree

Positive degree of C(229, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_229_2 : luebeckConwayPolynomial? 229 2 = some luebeckConwayPolynomial_229_2

Lookup identifies the imported C(229, 2).

def Hex.Conway.luebeckConwayPolynomial_557_2 : FpPoly 557

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

Equations

• Hex.Conway.luebeckConwayPolynomial_557_2 = { coeffs := #[2, 553, 1], normalized := Hex.Conway.luebeckConwayPolynomial_557_2._proof_1 }

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_557_2_monic : DensePoly.Monic luebeckConwayPolynomial_557_2

Monicity of C(557, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_557_2_degree_pos : 0 < luebeckConwayPolynomial_557_2.degree

Positive degree of C(557, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_557_2 : luebeckConwayPolynomial? 557 2 = some luebeckConwayPolynomial_557_2

Lookup identifies the imported C(557, 2).

def Hex.Conway.luebeckConwayPolynomial_607_2 : FpPoly 607

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

Equations

• Hex.Conway.luebeckConwayPolynomial_607_2 = { coeffs := #[3, 606, 1], normalized := Hex.Conway.luebeckConwayPolynomial_607_2._proof_1 }

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_607_2_monic : DensePoly.Monic luebeckConwayPolynomial_607_2

Monicity of C(607, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_607_2_degree_pos : 0 < luebeckConwayPolynomial_607_2.degree

Positive degree of C(607, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_607_2 : luebeckConwayPolynomial? 607 2 = some luebeckConwayPolynomial_607_2

Lookup identifies the imported C(607, 2).

def Hex.Conway.luebeckConwayPolynomial_653_2 : FpPoly 653

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

Equations

• Hex.Conway.luebeckConwayPolynomial_653_2 = { coeffs := #[2, 649, 1], normalized := Hex.Conway.luebeckConwayPolynomial_653_2._proof_1 }

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_653_2_monic : DensePoly.Monic luebeckConwayPolynomial_653_2

Monicity of C(653, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_653_2_degree_pos : 0 < luebeckConwayPolynomial_653_2.degree

Positive degree of C(653, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_653_2 : luebeckConwayPolynomial? 653 2 = some luebeckConwayPolynomial_653_2

Lookup identifies the imported C(653, 2).

def Hex.Conway.luebeckConwayPolynomial_733_2 : FpPoly 733

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

Equations

• Hex.Conway.luebeckConwayPolynomial_733_2 = { coeffs := #[6, 732, 1], normalized := Hex.Conway.luebeckConwayPolynomial_733_2._proof_1 }

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_733_2_monic : DensePoly.Monic luebeckConwayPolynomial_733_2

Monicity of C(733, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_733_2_degree_pos : 0 < luebeckConwayPolynomial_733_2.degree

Positive degree of C(733, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_733_2 : luebeckConwayPolynomial? 733 2 = some luebeckConwayPolynomial_733_2

Lookup identifies the imported C(733, 2).

def Hex.Conway.luebeckConwayPolynomial_787_2 : FpPoly 787

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

Equations

• Hex.Conway.luebeckConwayPolynomial_787_2 = { coeffs := #[2, 786, 1], normalized := Hex.Conway.luebeckConwayPolynomial_787_2._proof_1 }

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_787_2_monic : DensePoly.Monic luebeckConwayPolynomial_787_2

Monicity of C(787, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_787_2_degree_pos : 0 < luebeckConwayPolynomial_787_2.degree

Positive degree of C(787, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_787_2 : luebeckConwayPolynomial? 787 2 = some luebeckConwayPolynomial_787_2

Lookup identifies the imported C(787, 2).

def Hex.Conway.luebeckConwayPolynomial_887_2 : FpPoly 887

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

Equations

• Hex.Conway.luebeckConwayPolynomial_887_2 = { coeffs := #[5, 885, 1], normalized := Hex.Conway.luebeckConwayPolynomial_887_2._proof_1 }

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_887_2_monic : DensePoly.Monic luebeckConwayPolynomial_887_2

Monicity of C(887, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_887_2_degree_pos : 0 < luebeckConwayPolynomial_887_2.degree

Positive degree of C(887, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_887_2 : luebeckConwayPolynomial? 887 2 = some luebeckConwayPolynomial_887_2

Lookup identifies the imported C(887, 2).

def Hex.Conway.luebeckConwayPolynomial_983_2 : FpPoly 983

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

Equations

• Hex.Conway.luebeckConwayPolynomial_983_2 = { coeffs := #[5, 981, 1], normalized := Hex.Conway.luebeckConwayPolynomial_983_2._proof_1 }

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_983_2_monic : DensePoly.Monic luebeckConwayPolynomial_983_2

Monicity of C(983, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_983_2_degree_pos : 0 < luebeckConwayPolynomial_983_2.degree

Positive degree of C(983, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_983_2 : luebeckConwayPolynomial? 983 2 = some luebeckConwayPolynomial_983_2

Lookup identifies the imported C(983, 2).

def Hex.Conway.luebeckConwayPolynomial_271_2 : FpPoly 271

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

Equations

• Hex.Conway.luebeckConwayPolynomial_271_2 = { coeffs := #[6, 269, 1], normalized := Hex.Conway.luebeckConwayPolynomial_271_2._proof_1 }

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_271_2_monic : DensePoly.Monic luebeckConwayPolynomial_271_2

Monicity of C(271, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_271_2_degree_pos : 0 < luebeckConwayPolynomial_271_2.degree

Positive degree of C(271, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_271_2 : luebeckConwayPolynomial? 271 2 = some luebeckConwayPolynomial_271_2

Lookup identifies the imported C(271, 2).

def Hex.Conway.luebeckConwayPolynomial_313_2 : FpPoly 313

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

Equations

• Hex.Conway.luebeckConwayPolynomial_313_2 = { coeffs := #[10, 310, 1], normalized := Hex.Conway.luebeckConwayPolynomial_313_2._proof_1 }

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_313_2_monic : DensePoly.Monic luebeckConwayPolynomial_313_2

Monicity of C(313, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_313_2_degree_pos : 0 < luebeckConwayPolynomial_313_2.degree

Positive degree of C(313, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_313_2 : luebeckConwayPolynomial? 313 2 = some luebeckConwayPolynomial_313_2

Lookup identifies the imported C(313, 2).

def Hex.Conway.luebeckConwayPolynomial_353_2 : FpPoly 353

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

Equations

• Hex.Conway.luebeckConwayPolynomial_353_2 = { coeffs := #[3, 348, 1], normalized := Hex.Conway.luebeckConwayPolynomial_353_2._proof_1 }

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_353_2_monic : DensePoly.Monic luebeckConwayPolynomial_353_2

Monicity of C(353, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_353_2_degree_pos : 0 < luebeckConwayPolynomial_353_2.degree

Positive degree of C(353, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_353_2 : luebeckConwayPolynomial? 353 2 = some luebeckConwayPolynomial_353_2

Lookup identifies the imported C(353, 2).

def Hex.Conway.luebeckConwayPolynomial_401_2 : FpPoly 401

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

Equations

• Hex.Conway.luebeckConwayPolynomial_401_2 = { coeffs := #[3, 396, 1], normalized := Hex.Conway.luebeckConwayPolynomial_401_2._proof_1 }

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_401_2_monic : DensePoly.Monic luebeckConwayPolynomial_401_2

Monicity of C(401, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_401_2_degree_pos : 0 < luebeckConwayPolynomial_401_2.degree

Positive degree of C(401, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_401_2 : luebeckConwayPolynomial? 401 2 = some luebeckConwayPolynomial_401_2

Lookup identifies the imported C(401, 2).

def Hex.Conway.luebeckConwayPolynomial_457_2 : FpPoly 457

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

Equations

• Hex.Conway.luebeckConwayPolynomial_457_2 = { coeffs := #[13, 454, 1], normalized := Hex.Conway.luebeckConwayPolynomial_457_2._proof_1 }

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_457_2_monic : DensePoly.Monic luebeckConwayPolynomial_457_2

Monicity of C(457, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_457_2_degree_pos : 0 < luebeckConwayPolynomial_457_2.degree

Positive degree of C(457, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_457_2 : luebeckConwayPolynomial? 457 2 = some luebeckConwayPolynomial_457_2

Lookup identifies the imported C(457, 2).

def Hex.Conway.luebeckConwayPolynomial_503_2 : FpPoly 503

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

Equations

• Hex.Conway.luebeckConwayPolynomial_503_2 = { coeffs := #[5, 498, 1], normalized := Hex.Conway.luebeckConwayPolynomial_503_2._proof_1 }

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_503_2_monic : DensePoly.Monic luebeckConwayPolynomial_503_2

Monicity of C(503, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_503_2_degree_pos : 0 < luebeckConwayPolynomial_503_2.degree

Positive degree of C(503, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_503_2 : luebeckConwayPolynomial? 503 2 = some luebeckConwayPolynomial_503_2

Lookup identifies the imported C(503, 2).

def Hex.Conway.luebeckConwayPolynomial_149_2 : FpPoly 149

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

Equations

• Hex.Conway.luebeckConwayPolynomial_149_2 = { coeffs := #[2, 145, 1], normalized := Hex.Conway.luebeckConwayPolynomial_149_2._proof_1 }

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_149_2_monic : DensePoly.Monic luebeckConwayPolynomial_149_2

Monicity of C(149, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_149_2_degree_pos : 0 < luebeckConwayPolynomial_149_2.degree

Positive degree of C(149, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_149_2 : luebeckConwayPolynomial? 149 2 = some luebeckConwayPolynomial_149_2

Lookup identifies the imported C(149, 2).

def Hex.Conway.luebeckConwayPolynomial_173_2 : FpPoly 173

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

Equations

• Hex.Conway.luebeckConwayPolynomial_173_2 = { coeffs := #[2, 169, 1], normalized := Hex.Conway.luebeckConwayPolynomial_173_2._proof_1 }

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_173_2_monic : DensePoly.Monic luebeckConwayPolynomial_173_2

Monicity of C(173, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_173_2_degree_pos : 0 < luebeckConwayPolynomial_173_2.degree

Positive degree of C(173, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_173_2 : luebeckConwayPolynomial? 173 2 = some luebeckConwayPolynomial_173_2

Lookup identifies the imported C(173, 2).

def Hex.Conway.luebeckConwayPolynomial_199_2 : FpPoly 199

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

Equations

• Hex.Conway.luebeckConwayPolynomial_199_2 = { coeffs := #[3, 193, 1], normalized := Hex.Conway.luebeckConwayPolynomial_199_2._proof_1 }

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_199_2_monic : DensePoly.Monic luebeckConwayPolynomial_199_2

Monicity of C(199, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_199_2_degree_pos : 0 < luebeckConwayPolynomial_199_2.degree

Positive degree of C(199, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_199_2 : luebeckConwayPolynomial? 199 2 = some luebeckConwayPolynomial_199_2

Lookup identifies the imported C(199, 2).

def Hex.Conway.luebeckConwayPolynomial_241_2 : FpPoly 241

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

Equations

• Hex.Conway.luebeckConwayPolynomial_241_2 = { coeffs := #[7, 238, 1], normalized := Hex.Conway.luebeckConwayPolynomial_241_2._proof_1 }

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_241_2_monic : DensePoly.Monic luebeckConwayPolynomial_241_2

Monicity of C(241, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_241_2_degree_pos : 0 < luebeckConwayPolynomial_241_2.degree

Positive degree of C(241, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_241_2 : luebeckConwayPolynomial? 241 2 = some luebeckConwayPolynomial_241_2

Lookup identifies the imported C(241, 2).

def Hex.Conway.luebeckConwayPolynomial_577_2 : FpPoly 577

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

Equations

• Hex.Conway.luebeckConwayPolynomial_577_2 = { coeffs := #[5, 572, 1], normalized := Hex.Conway.luebeckConwayPolynomial_577_2._proof_1 }

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_577_2_monic : DensePoly.Monic luebeckConwayPolynomial_577_2

Monicity of C(577, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_577_2_degree_pos : 0 < luebeckConwayPolynomial_577_2.degree

Positive degree of C(577, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_577_2 : luebeckConwayPolynomial? 577 2 = some luebeckConwayPolynomial_577_2

Lookup identifies the imported C(577, 2).

def Hex.Conway.luebeckConwayPolynomial_79_2 : FpPoly 79

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

Equations

• Hex.Conway.luebeckConwayPolynomial_79_2 = { coeffs := #[3, 78, 1], normalized := Hex.Conway.luebeckConwayPolynomial_79_2._proof_1 }

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_79_2_monic : DensePoly.Monic luebeckConwayPolynomial_79_2

Monicity of C(79, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_79_2_degree_pos : 0 < luebeckConwayPolynomial_79_2.degree

Positive degree of C(79, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_79_2 : luebeckConwayPolynomial? 79 2 = some luebeckConwayPolynomial_79_2

Lookup identifies the imported C(79, 2).

def Hex.Conway.luebeckConwayPolynomial_101_2 : FpPoly 101

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

Equations

• Hex.Conway.luebeckConwayPolynomial_101_2 = { coeffs := #[2, 97, 1], normalized := Hex.Conway.luebeckConwayPolynomial_101_2._proof_1 }

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_101_2_monic : DensePoly.Monic luebeckConwayPolynomial_101_2

Monicity of C(101, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_101_2_degree_pos : 0 < luebeckConwayPolynomial_101_2.degree

Positive degree of C(101, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_101_2 : luebeckConwayPolynomial? 101 2 = some luebeckConwayPolynomial_101_2

Lookup identifies the imported C(101, 2).