def Hex.Conway.luebeckConwayPolynomial_521_3 : FpPoly 521

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

Equations

• Hex.Conway.luebeckConwayPolynomial_521_3 = { coeffs := #[518, 4, 0, 1], normalized := Hex.Conway.luebeckConwayPolynomial_521_3._proof_1 }

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_521_3_monic : DensePoly.Monic luebeckConwayPolynomial_521_3

Monicity of C(521, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_521_3_degree_pos : 0 < luebeckConwayPolynomial_521_3.degree

Positive degree of C(521, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_521_3 : luebeckConwayPolynomial? 521 3 = some luebeckConwayPolynomial_521_3

Lookup identifies the imported C(521, 3).

def Hex.Conway.luebeckConwayPolynomial_601_3 : FpPoly 601

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_601_3_monic : DensePoly.Monic luebeckConwayPolynomial_601_3

Monicity of C(601, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_601_3_degree_pos : 0 < luebeckConwayPolynomial_601_3.degree

Positive degree of C(601, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_601_3 : luebeckConwayPolynomial? 601 3 = some luebeckConwayPolynomial_601_3

Lookup identifies the imported C(601, 3).

def Hex.Conway.luebeckConwayPolynomial_619_3 : FpPoly 619

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

Equations

• Hex.Conway.luebeckConwayPolynomial_619_3 = { coeffs := #[617, 6, 0, 1], normalized := Hex.Conway.luebeckConwayPolynomial_619_3._proof_1 }

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_619_3_monic : DensePoly.Monic luebeckConwayPolynomial_619_3

Monicity of C(619, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_619_3_degree_pos : 0 < luebeckConwayPolynomial_619_3.degree

Positive degree of C(619, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_619_3 : luebeckConwayPolynomial? 619 3 = some luebeckConwayPolynomial_619_3

Lookup identifies the imported C(619, 3).

def Hex.Conway.luebeckConwayPolynomial_659_3 : FpPoly 659

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

Equations

• Hex.Conway.luebeckConwayPolynomial_659_3 = { coeffs := #[657, 2, 0, 1], normalized := Hex.Conway.luebeckConwayPolynomial_659_3._proof_1 }

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_659_3_monic : DensePoly.Monic luebeckConwayPolynomial_659_3

Monicity of C(659, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_659_3_degree_pos : 0 < luebeckConwayPolynomial_659_3.degree

Positive degree of C(659, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_659_3 : luebeckConwayPolynomial? 659 3 = some luebeckConwayPolynomial_659_3

Lookup identifies the imported C(659, 3).

def Hex.Conway.luebeckConwayPolynomial_733_3 : FpPoly 733

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

Equations

• Hex.Conway.luebeckConwayPolynomial_733_3 = { coeffs := #[727, 4, 0, 1], normalized := Hex.Conway.luebeckConwayPolynomial_733_3._proof_1 }

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_733_3_monic : DensePoly.Monic luebeckConwayPolynomial_733_3

Monicity of C(733, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_733_3_degree_pos : 0 < luebeckConwayPolynomial_733_3.degree

Positive degree of C(733, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_733_3 : luebeckConwayPolynomial? 733 3 = some luebeckConwayPolynomial_733_3

Lookup identifies the imported C(733, 3).

def Hex.Conway.luebeckConwayPolynomial_787_3 : FpPoly 787

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

Equations

• Hex.Conway.luebeckConwayPolynomial_787_3 = { coeffs := #[785, 2, 0, 1], normalized := Hex.Conway.luebeckConwayPolynomial_787_3._proof_1 }

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_787_3_monic : DensePoly.Monic luebeckConwayPolynomial_787_3

Monicity of C(787, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_787_3_degree_pos : 0 < luebeckConwayPolynomial_787_3.degree

Positive degree of C(787, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_787_3 : luebeckConwayPolynomial? 787 3 = some luebeckConwayPolynomial_787_3

Lookup identifies the imported C(787, 3).

def Hex.Conway.luebeckConwayPolynomial_881_3 : FpPoly 881

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_881_3_monic : DensePoly.Monic luebeckConwayPolynomial_881_3

Monicity of C(881, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_881_3_degree_pos : 0 < luebeckConwayPolynomial_881_3.degree

Positive degree of C(881, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_881_3 : luebeckConwayPolynomial? 881 3 = some luebeckConwayPolynomial_881_3

Lookup identifies the imported C(881, 3).

def Hex.Conway.luebeckConwayPolynomial_953_3 : FpPoly 953

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

Equations

• Hex.Conway.luebeckConwayPolynomial_953_3 = { coeffs := #[950, 7, 0, 1], normalized := Hex.Conway.luebeckConwayPolynomial_953_3._proof_1 }

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_953_3_monic : DensePoly.Monic luebeckConwayPolynomial_953_3

Monicity of C(953, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_953_3_degree_pos : 0 < luebeckConwayPolynomial_953_3.degree

Positive degree of C(953, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_953_3 : luebeckConwayPolynomial? 953 3 = some luebeckConwayPolynomial_953_3

Lookup identifies the imported C(953, 3).

def Hex.Conway.luebeckConwayPolynomial_19_4 : FpPoly 19

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

Equations

• Hex.Conway.luebeckConwayPolynomial_19_4 = { coeffs := #[2, 11, 2, 0, 1], normalized := Hex.Conway.luebeckConwayPolynomial_19_4._proof_1 }

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_19_4_monic : DensePoly.Monic luebeckConwayPolynomial_19_4

Monicity of C(19, 4).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_19_4_degree_pos : 0 < luebeckConwayPolynomial_19_4.degree

Positive degree of C(19, 4).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_19_4 : luebeckConwayPolynomial? 19 4 = some luebeckConwayPolynomial_19_4

Lookup identifies the imported C(19, 4).

def Hex.Conway.luebeckConwayPolynomial_283_3 : FpPoly 283

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_283_3_monic : DensePoly.Monic luebeckConwayPolynomial_283_3

Monicity of C(283, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_283_3_degree_pos : 0 < luebeckConwayPolynomial_283_3.degree

Positive degree of C(283, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_283_3 : luebeckConwayPolynomial? 283 3 = some luebeckConwayPolynomial_283_3

Lookup identifies the imported C(283, 3).

def Hex.Conway.luebeckConwayPolynomial_347_3 : FpPoly 347

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

Equations

• Hex.Conway.luebeckConwayPolynomial_347_3 = { coeffs := #[345, 9, 0, 1], normalized := Hex.Conway.luebeckConwayPolynomial_347_3._proof_1 }

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_347_3_monic : DensePoly.Monic luebeckConwayPolynomial_347_3

Monicity of C(347, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_347_3_degree_pos : 0 < luebeckConwayPolynomial_347_3.degree

Positive degree of C(347, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_347_3 : luebeckConwayPolynomial? 347 3 = some luebeckConwayPolynomial_347_3

Lookup identifies the imported C(347, 3).

def Hex.Conway.luebeckConwayPolynomial_379_3 : FpPoly 379

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

Equations

• Hex.Conway.luebeckConwayPolynomial_379_3 = { coeffs := #[377, 5, 0, 1], normalized := Hex.Conway.luebeckConwayPolynomial_379_3._proof_1 }

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_379_3_monic : DensePoly.Monic luebeckConwayPolynomial_379_3

Monicity of C(379, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_379_3_degree_pos : 0 < luebeckConwayPolynomial_379_3.degree

Positive degree of C(379, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_379_3 : luebeckConwayPolynomial? 379 3 = some luebeckConwayPolynomial_379_3

Lookup identifies the imported C(379, 3).

def Hex.Conway.luebeckConwayPolynomial_439_3 : FpPoly 439

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

Equations

• Hex.Conway.luebeckConwayPolynomial_439_3 = { coeffs := #[424, 3, 0, 1], normalized := Hex.Conway.luebeckConwayPolynomial_439_3._proof_1 }

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_439_3_monic : DensePoly.Monic luebeckConwayPolynomial_439_3

Monicity of C(439, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_439_3_degree_pos : 0 < luebeckConwayPolynomial_439_3.degree

Positive degree of C(439, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_439_3 : luebeckConwayPolynomial? 439 3 = some luebeckConwayPolynomial_439_3

Lookup identifies the imported C(439, 3).

def Hex.Conway.luebeckConwayPolynomial_491_3 : FpPoly 491

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

Equations

• Hex.Conway.luebeckConwayPolynomial_491_3 = { coeffs := #[489, 2, 0, 1], normalized := Hex.Conway.luebeckConwayPolynomial_491_3._proof_1 }

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_491_3_monic : DensePoly.Monic luebeckConwayPolynomial_491_3

Monicity of C(491, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_491_3_degree_pos : 0 < luebeckConwayPolynomial_491_3.degree

Positive degree of C(491, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_491_3 : luebeckConwayPolynomial? 491 3 = some luebeckConwayPolynomial_491_3

Lookup identifies the imported C(491, 3).

def Hex.Conway.luebeckConwayPolynomial_137_3 : FpPoly 137

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

Equations

• Hex.Conway.luebeckConwayPolynomial_137_3 = { coeffs := #[134, 6, 0, 1], normalized := Hex.Conway.luebeckConwayPolynomial_137_3._proof_1 }

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_137_3_monic : DensePoly.Monic luebeckConwayPolynomial_137_3

Monicity of C(137, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_137_3_degree_pos : 0 < luebeckConwayPolynomial_137_3.degree

Positive degree of C(137, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_137_3 : luebeckConwayPolynomial? 137 3 = some luebeckConwayPolynomial_137_3

Lookup identifies the imported C(137, 3).

def Hex.Conway.luebeckConwayPolynomial_163_3 : FpPoly 163

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

Equations

• Hex.Conway.luebeckConwayPolynomial_163_3 = { coeffs := #[161, 7, 0, 1], normalized := Hex.Conway.luebeckConwayPolynomial_163_3._proof_1 }

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_163_3_monic : DensePoly.Monic luebeckConwayPolynomial_163_3

Monicity of C(163, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_163_3_degree_pos : 0 < luebeckConwayPolynomial_163_3.degree

Positive degree of C(163, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_163_3 : luebeckConwayPolynomial? 163 3 = some luebeckConwayPolynomial_163_3

Lookup identifies the imported C(163, 3).

def Hex.Conway.luebeckConwayPolynomial_557_3 : FpPoly 557

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

Equations

• Hex.Conway.luebeckConwayPolynomial_557_3 = { coeffs := #[555, 3, 0, 1], normalized := Hex.Conway.luebeckConwayPolynomial_557_3._proof_1 }

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_557_3_monic : DensePoly.Monic luebeckConwayPolynomial_557_3

Monicity of C(557, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_557_3_degree_pos : 0 < luebeckConwayPolynomial_557_3.degree

Positive degree of C(557, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_557_3 : luebeckConwayPolynomial? 557 3 = some luebeckConwayPolynomial_557_3

Lookup identifies the imported C(557, 3).

def Hex.Conway.luebeckConwayPolynomial_587_3 : FpPoly 587

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

Equations

• Hex.Conway.luebeckConwayPolynomial_587_3 = { coeffs := #[585, 3, 0, 1], normalized := Hex.Conway.luebeckConwayPolynomial_587_3._proof_1 }

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_587_3_monic : DensePoly.Monic luebeckConwayPolynomial_587_3

Monicity of C(587, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_587_3_degree_pos : 0 < luebeckConwayPolynomial_587_3.degree

Positive degree of C(587, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_587_3 : luebeckConwayPolynomial? 587 3 = some luebeckConwayPolynomial_587_3

Lookup identifies the imported C(587, 3).

def Hex.Conway.luebeckConwayPolynomial_701_3 : FpPoly 701

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

Equations

• Hex.Conway.luebeckConwayPolynomial_701_3 = { coeffs := #[699, 2, 0, 1], normalized := Hex.Conway.luebeckConwayPolynomial_701_3._proof_1 }

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_701_3_monic : DensePoly.Monic luebeckConwayPolynomial_701_3

Monicity of C(701, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_701_3_degree_pos : 0 < luebeckConwayPolynomial_701_3.degree

Positive degree of C(701, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_701_3 : luebeckConwayPolynomial? 701 3 = some luebeckConwayPolynomial_701_3

Lookup identifies the imported C(701, 3).

def Hex.Conway.luebeckConwayPolynomial_761_3 : FpPoly 761

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

Equations

• Hex.Conway.luebeckConwayPolynomial_761_3 = { coeffs := #[755, 12, 0, 1], normalized := Hex.Conway.luebeckConwayPolynomial_761_3._proof_1 }

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_761_3_monic : DensePoly.Monic luebeckConwayPolynomial_761_3

Monicity of C(761, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_761_3_degree_pos : 0 < luebeckConwayPolynomial_761_3.degree

Positive degree of C(761, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_761_3 : luebeckConwayPolynomial? 761 3 = some luebeckConwayPolynomial_761_3

Lookup identifies the imported C(761, 3).

def Hex.Conway.luebeckConwayPolynomial_863_3 : FpPoly 863

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

Equations

• Hex.Conway.luebeckConwayPolynomial_863_3 = { coeffs := #[858, 5, 0, 1], normalized := Hex.Conway.luebeckConwayPolynomial_863_3._proof_1 }

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_863_3_monic : DensePoly.Monic luebeckConwayPolynomial_863_3

Monicity of C(863, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_863_3_degree_pos : 0 < luebeckConwayPolynomial_863_3.degree

Positive degree of C(863, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_863_3 : luebeckConwayPolynomial? 863 3 = some luebeckConwayPolynomial_863_3

Lookup identifies the imported C(863, 3).

def Hex.Conway.luebeckConwayPolynomial_937_3 : FpPoly 937

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

Equations

• Hex.Conway.luebeckConwayPolynomial_937_3 = { coeffs := #[932, 3, 0, 1], normalized := Hex.Conway.luebeckConwayPolynomial_937_3._proof_1 }

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_937_3_monic : DensePoly.Monic luebeckConwayPolynomial_937_3

Monicity of C(937, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_937_3_degree_pos : 0 < luebeckConwayPolynomial_937_3.degree

Positive degree of C(937, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_937_3 : luebeckConwayPolynomial? 937 3 = some luebeckConwayPolynomial_937_3

Lookup identifies the imported C(937, 3).

def Hex.Conway.luebeckConwayPolynomial_271_3 : FpPoly 271

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

Equations

• Hex.Conway.luebeckConwayPolynomial_271_3 = { coeffs := #[265, 2, 0, 1], normalized := Hex.Conway.luebeckConwayPolynomial_271_3._proof_1 }

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_271_3_monic : DensePoly.Monic luebeckConwayPolynomial_271_3

Monicity of C(271, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_271_3_degree_pos : 0 < luebeckConwayPolynomial_271_3.degree

Positive degree of C(271, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_271_3 : luebeckConwayPolynomial? 271 3 = some luebeckConwayPolynomial_271_3

Lookup identifies the imported C(271, 3).

def Hex.Conway.luebeckConwayPolynomial_317_3 : FpPoly 317

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

Equations

• Hex.Conway.luebeckConwayPolynomial_317_3 = { coeffs := #[315, 7, 0, 1], normalized := Hex.Conway.luebeckConwayPolynomial_317_3._proof_1 }

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_317_3_monic : DensePoly.Monic luebeckConwayPolynomial_317_3

Monicity of C(317, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_317_3_degree_pos : 0 < luebeckConwayPolynomial_317_3.degree

Positive degree of C(317, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_317_3 : luebeckConwayPolynomial? 317 3 = some luebeckConwayPolynomial_317_3

Lookup identifies the imported C(317, 3).