def Hex.Conway.luebeckConwayPolynomial_947_2 : FpPoly 947

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_947_2_monic : DensePoly.Monic luebeckConwayPolynomial_947_2

Monicity of C(947, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_947_2_degree_pos : 0 < luebeckConwayPolynomial_947_2.degree

Positive degree of C(947, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_947_2 : luebeckConwayPolynomial? 947 2 = some luebeckConwayPolynomial_947_2

Lookup identifies the imported C(947, 2).

def Hex.Conway.luebeckConwayPolynomial_281_2 : FpPoly 281

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_281_2_monic : DensePoly.Monic luebeckConwayPolynomial_281_2

Monicity of C(281, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_281_2_degree_pos : 0 < luebeckConwayPolynomial_281_2.degree

Positive degree of C(281, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_281_2 : luebeckConwayPolynomial? 281 2 = some luebeckConwayPolynomial_281_2

Lookup identifies the imported C(281, 2).

def Hex.Conway.luebeckConwayPolynomial_311_2 : FpPoly 311

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_311_2_monic : DensePoly.Monic luebeckConwayPolynomial_311_2

Monicity of C(311, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_311_2_degree_pos : 0 < luebeckConwayPolynomial_311_2.degree

Positive degree of C(311, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_311_2 : luebeckConwayPolynomial? 311 2 = some luebeckConwayPolynomial_311_2

Lookup identifies the imported C(311, 2).

def Hex.Conway.luebeckConwayPolynomial_379_2 : FpPoly 379

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_379_2_monic : DensePoly.Monic luebeckConwayPolynomial_379_2

Monicity of C(379, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_379_2_degree_pos : 0 < luebeckConwayPolynomial_379_2.degree

Positive degree of C(379, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_379_2 : luebeckConwayPolynomial? 379 2 = some luebeckConwayPolynomial_379_2

Lookup identifies the imported C(379, 2).

def Hex.Conway.luebeckConwayPolynomial_439_2 : FpPoly 439

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

Equations

• Hex.Conway.luebeckConwayPolynomial_439_2 = { coeffs := #[15, 436, 1], normalized := Hex.Conway.luebeckConwayPolynomial_439_2._proof_1 }

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_439_2_monic : DensePoly.Monic luebeckConwayPolynomial_439_2

Monicity of C(439, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_439_2_degree_pos : 0 < luebeckConwayPolynomial_439_2.degree

Positive degree of C(439, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_439_2 : luebeckConwayPolynomial? 439 2 = some luebeckConwayPolynomial_439_2

Lookup identifies the imported C(439, 2).

def Hex.Conway.luebeckConwayPolynomial_509_2 : FpPoly 509

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_509_2_monic : DensePoly.Monic luebeckConwayPolynomial_509_2

Monicity of C(509, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_509_2_degree_pos : 0 < luebeckConwayPolynomial_509_2.degree

Positive degree of C(509, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_509_2 : luebeckConwayPolynomial? 509 2 = some luebeckConwayPolynomial_509_2

Lookup identifies the imported C(509, 2).

def Hex.Conway.luebeckConwayPolynomial_239_2 : FpPoly 239

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_239_2_monic : DensePoly.Monic luebeckConwayPolynomial_239_2

Monicity of C(239, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_239_2_degree_pos : 0 < luebeckConwayPolynomial_239_2.degree

Positive degree of C(239, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_239_2 : luebeckConwayPolynomial? 239 2 = some luebeckConwayPolynomial_239_2

Lookup identifies the imported C(239, 2).

def Hex.Conway.luebeckConwayPolynomial_563_2 : FpPoly 563

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_563_2_monic : DensePoly.Monic luebeckConwayPolynomial_563_2

Monicity of C(563, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_563_2_degree_pos : 0 < luebeckConwayPolynomial_563_2.degree

Positive degree of C(563, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_563_2 : luebeckConwayPolynomial? 563 2 = some luebeckConwayPolynomial_563_2

Lookup identifies the imported C(563, 2).

def Hex.Conway.luebeckConwayPolynomial_613_2 : FpPoly 613

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_613_2_monic : DensePoly.Monic luebeckConwayPolynomial_613_2

Monicity of C(613, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_613_2_degree_pos : 0 < luebeckConwayPolynomial_613_2.degree

Positive degree of C(613, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_613_2 : luebeckConwayPolynomial? 613 2 = some luebeckConwayPolynomial_613_2

Lookup identifies the imported C(613, 2).

def Hex.Conway.luebeckConwayPolynomial_673_2 : FpPoly 673

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_673_2_monic : DensePoly.Monic luebeckConwayPolynomial_673_2

Monicity of C(673, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_673_2_degree_pos : 0 < luebeckConwayPolynomial_673_2.degree

Positive degree of C(673, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_673_2 : luebeckConwayPolynomial? 673 2 = some luebeckConwayPolynomial_673_2

Lookup identifies the imported C(673, 2).

def Hex.Conway.luebeckConwayPolynomial_751_2 : FpPoly 751

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_751_2_monic : DensePoly.Monic luebeckConwayPolynomial_751_2

Monicity of C(751, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_751_2_degree_pos : 0 < luebeckConwayPolynomial_751_2.degree

Positive degree of C(751, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_751_2 : luebeckConwayPolynomial? 751 2 = some luebeckConwayPolynomial_751_2

Lookup identifies the imported C(751, 2).

def Hex.Conway.luebeckConwayPolynomial_809_2 : FpPoly 809

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_809_2_monic : DensePoly.Monic luebeckConwayPolynomial_809_2

Monicity of C(809, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_809_2_degree_pos : 0 < luebeckConwayPolynomial_809_2.degree

Positive degree of C(809, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_809_2 : luebeckConwayPolynomial? 809 2 = some luebeckConwayPolynomial_809_2

Lookup identifies the imported C(809, 2).

def Hex.Conway.luebeckConwayPolynomial_907_2 : FpPoly 907

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_907_2_monic : DensePoly.Monic luebeckConwayPolynomial_907_2

Monicity of C(907, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_907_2_degree_pos : 0 < luebeckConwayPolynomial_907_2.degree

Positive degree of C(907, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_907_2 : luebeckConwayPolynomial? 907 2 = some luebeckConwayPolynomial_907_2

Lookup identifies the imported C(907, 2).

def Hex.Conway.luebeckConwayPolynomial_997_2 : FpPoly 997

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_997_2_monic : DensePoly.Monic luebeckConwayPolynomial_997_2

Monicity of C(997, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_997_2_degree_pos : 0 < luebeckConwayPolynomial_997_2.degree

Positive degree of C(997, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_997_2 : luebeckConwayPolynomial? 997 2 = some luebeckConwayPolynomial_997_2

Lookup identifies the imported C(997, 2).

def Hex.Conway.luebeckConwayPolynomial_277_2 : FpPoly 277

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_277_2_monic : DensePoly.Monic luebeckConwayPolynomial_277_2

Monicity of C(277, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_277_2_degree_pos : 0 < luebeckConwayPolynomial_277_2.degree

Positive degree of C(277, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_277_2 : luebeckConwayPolynomial? 277 2 = some luebeckConwayPolynomial_277_2

Lookup identifies the imported C(277, 2).

def Hex.Conway.luebeckConwayPolynomial_317_2 : FpPoly 317

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_317_2_monic : DensePoly.Monic luebeckConwayPolynomial_317_2

Monicity of C(317, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_317_2_degree_pos : 0 < luebeckConwayPolynomial_317_2.degree

Positive degree of C(317, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_317_2 : luebeckConwayPolynomial? 317 2 = some luebeckConwayPolynomial_317_2

Lookup identifies the imported C(317, 2).

def Hex.Conway.luebeckConwayPolynomial_359_2 : FpPoly 359

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_359_2_monic : DensePoly.Monic luebeckConwayPolynomial_359_2

Monicity of C(359, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_359_2_degree_pos : 0 < luebeckConwayPolynomial_359_2.degree

Positive degree of C(359, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_359_2 : luebeckConwayPolynomial? 359 2 = some luebeckConwayPolynomial_359_2

Lookup identifies the imported C(359, 2).

def Hex.Conway.luebeckConwayPolynomial_431_2 : FpPoly 431

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_431_2_monic : DensePoly.Monic luebeckConwayPolynomial_431_2

Monicity of C(431, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_431_2_degree_pos : 0 < luebeckConwayPolynomial_431_2.degree

Positive degree of C(431, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_431_2 : luebeckConwayPolynomial? 431 2 = some luebeckConwayPolynomial_431_2

Lookup identifies the imported C(431, 2).

def Hex.Conway.luebeckConwayPolynomial_467_2 : FpPoly 467

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_467_2_monic : DensePoly.Monic luebeckConwayPolynomial_467_2

Monicity of C(467, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_467_2_degree_pos : 0 < luebeckConwayPolynomial_467_2.degree

Positive degree of C(467, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_467_2 : luebeckConwayPolynomial? 467 2 = some luebeckConwayPolynomial_467_2

Lookup identifies the imported C(467, 2).

def Hex.Conway.luebeckConwayPolynomial_17_3 : FpPoly 17

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

Equations

• Hex.Conway.luebeckConwayPolynomial_17_3 = { coeffs := #[14, 1, 0, 1], normalized := Hex.Conway.luebeckConwayPolynomial_17_3._proof_1 }

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_17_3_monic : DensePoly.Monic luebeckConwayPolynomial_17_3

Monicity of C(17, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_17_3_degree_pos : 0 < luebeckConwayPolynomial_17_3.degree

Positive degree of C(17, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_17_3 : luebeckConwayPolynomial? 17 3 = some luebeckConwayPolynomial_17_3

Lookup identifies the imported C(17, 3).

def Hex.Conway.luebeckConwayPolynomial_137_2 : FpPoly 137

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_137_2_monic : DensePoly.Monic luebeckConwayPolynomial_137_2

Monicity of C(137, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_137_2_degree_pos : 0 < luebeckConwayPolynomial_137_2.degree

Positive degree of C(137, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_137_2 : luebeckConwayPolynomial? 137 2 = some luebeckConwayPolynomial_137_2

Lookup identifies the imported C(137, 2).

def Hex.Conway.luebeckConwayPolynomial_167_2 : FpPoly 167

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_167_2_monic : DensePoly.Monic luebeckConwayPolynomial_167_2

Monicity of C(167, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_167_2_degree_pos : 0 < luebeckConwayPolynomial_167_2.degree

Positive degree of C(167, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_167_2 : luebeckConwayPolynomial? 167 2 = some luebeckConwayPolynomial_167_2

Lookup identifies the imported C(167, 2).

def Hex.Conway.luebeckConwayPolynomial_197_2 : FpPoly 197

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_197_2_monic : DensePoly.Monic luebeckConwayPolynomial_197_2

Monicity of C(197, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_197_2_degree_pos : 0 < luebeckConwayPolynomial_197_2.degree

Positive degree of C(197, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_197_2 : luebeckConwayPolynomial? 197 2 = some luebeckConwayPolynomial_197_2

Lookup identifies the imported C(197, 2).

def Hex.Conway.luebeckConwayPolynomial_233_2 : FpPoly 233

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_233_2_monic : DensePoly.Monic luebeckConwayPolynomial_233_2

Monicity of C(233, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_233_2_degree_pos : 0 < luebeckConwayPolynomial_233_2.degree

Positive degree of C(233, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_233_2 : luebeckConwayPolynomial? 233 2 = some luebeckConwayPolynomial_233_2

Lookup identifies the imported C(233, 2).