def Hex.Conway.luebeckConwayPolynomial_353_3 : FpPoly 353

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_353_3_monic : DensePoly.Monic luebeckConwayPolynomial_353_3

Monicity of C(353, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_353_3_degree_pos : 0 < luebeckConwayPolynomial_353_3.degree

Positive degree of C(353, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_353_3 : luebeckConwayPolynomial? 353 3 = some luebeckConwayPolynomial_353_3

Lookup identifies the imported C(353, 3).

def Hex.Conway.luebeckConwayPolynomial_433_3 : FpPoly 433

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_433_3_monic : DensePoly.Monic luebeckConwayPolynomial_433_3

Monicity of C(433, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_433_3_degree_pos : 0 < luebeckConwayPolynomial_433_3.degree

Positive degree of C(433, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_433_3 : luebeckConwayPolynomial? 433 3 = some luebeckConwayPolynomial_433_3

Lookup identifies the imported C(433, 3).

def Hex.Conway.luebeckConwayPolynomial_487_3 : FpPoly 487

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_487_3_monic : DensePoly.Monic luebeckConwayPolynomial_487_3

Monicity of C(487, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_487_3_degree_pos : 0 < luebeckConwayPolynomial_487_3.degree

Positive degree of C(487, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_487_3 : luebeckConwayPolynomial? 487 3 = some luebeckConwayPolynomial_487_3

Lookup identifies the imported C(487, 3).

def Hex.Conway.luebeckConwayPolynomial_79_3 : FpPoly 79

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_79_3_monic : DensePoly.Monic luebeckConwayPolynomial_79_3

Monicity of C(79, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_79_3_degree_pos : 0 < luebeckConwayPolynomial_79_3.degree

Positive degree of C(79, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_79_3 : luebeckConwayPolynomial? 79 3 = some luebeckConwayPolynomial_79_3

Lookup identifies the imported C(79, 3).

def Hex.Conway.luebeckConwayPolynomial_157_3 : FpPoly 157

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_157_3_monic : DensePoly.Monic luebeckConwayPolynomial_157_3

Monicity of C(157, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_157_3_degree_pos : 0 < luebeckConwayPolynomial_157_3.degree

Positive degree of C(157, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_157_3 : luebeckConwayPolynomial? 157 3 = some luebeckConwayPolynomial_157_3

Lookup identifies the imported C(157, 3).

def Hex.Conway.luebeckConwayPolynomial_199_3 : FpPoly 199

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_199_3_monic : DensePoly.Monic luebeckConwayPolynomial_199_3

Monicity of C(199, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_199_3_degree_pos : 0 < luebeckConwayPolynomial_199_3.degree

Positive degree of C(199, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_199_3 : luebeckConwayPolynomial? 199 3 = some luebeckConwayPolynomial_199_3

Lookup identifies the imported C(199, 3).

def Hex.Conway.luebeckConwayPolynomial_241_3 : FpPoly 241

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_241_3_monic : DensePoly.Monic luebeckConwayPolynomial_241_3

Monicity of C(241, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_241_3_degree_pos : 0 < luebeckConwayPolynomial_241_3.degree

Positive degree of C(241, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_241_3 : luebeckConwayPolynomial? 241 3 = some luebeckConwayPolynomial_241_3

Lookup identifies the imported C(241, 3).

def Hex.Conway.luebeckConwayPolynomial_773_3 : FpPoly 773

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_773_3_monic : DensePoly.Monic luebeckConwayPolynomial_773_3

Monicity of C(773, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_773_3_degree_pos : 0 < luebeckConwayPolynomial_773_3.degree

Positive degree of C(773, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_773_3 : luebeckConwayPolynomial? 773 3 = some luebeckConwayPolynomial_773_3

Lookup identifies the imported C(773, 3).

def Hex.Conway.luebeckConwayPolynomial_83_3 : FpPoly 83

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_83_3_monic : DensePoly.Monic luebeckConwayPolynomial_83_3

Monicity of C(83, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_83_3_degree_pos : 0 < luebeckConwayPolynomial_83_3.degree

Positive degree of C(83, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_83_3 : luebeckConwayPolynomial? 83 3 = some luebeckConwayPolynomial_83_3

Lookup identifies the imported C(83, 3).

def Hex.Conway.luebeckConwayPolynomial_127_3 : FpPoly 127

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_127_3_monic : DensePoly.Monic luebeckConwayPolynomial_127_3

Monicity of C(127, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_127_3_degree_pos : 0 < luebeckConwayPolynomial_127_3.degree

Positive degree of C(127, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_127_3 : luebeckConwayPolynomial? 127 3 = some luebeckConwayPolynomial_127_3

Lookup identifies the imported C(127, 3).

def Hex.Conway.luebeckConwayPolynomial_37_3 : FpPoly 37

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_37_3_monic : DensePoly.Monic luebeckConwayPolynomial_37_3

Monicity of C(37, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_37_3_degree_pos : 0 < luebeckConwayPolynomial_37_3.degree

Positive degree of C(37, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_37_3 : luebeckConwayPolynomial? 37 3 = some luebeckConwayPolynomial_37_3

Lookup identifies the imported C(37, 3).

def Hex.Conway.luebeckConwayPolynomial_43_3 : FpPoly 43

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_43_3_monic : DensePoly.Monic luebeckConwayPolynomial_43_3

Monicity of C(43, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_43_3_degree_pos : 0 < luebeckConwayPolynomial_43_3.degree

Positive degree of C(43, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_43_3 : luebeckConwayPolynomial? 43 3 = some luebeckConwayPolynomial_43_3

Lookup identifies the imported C(43, 3).

def Hex.Conway.luebeckConwayPolynomial_173_3 : FpPoly 173

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_173_3_monic : DensePoly.Monic luebeckConwayPolynomial_173_3

Monicity of C(173, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_173_3_degree_pos : 0 < luebeckConwayPolynomial_173_3.degree

Positive degree of C(173, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_173_3 : luebeckConwayPolynomial? 173 3 = some luebeckConwayPolynomial_173_3

Lookup identifies the imported C(173, 3).

def Hex.Conway.luebeckConwayPolynomial_23_3 : FpPoly 23

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_23_3_monic : DensePoly.Monic luebeckConwayPolynomial_23_3

Monicity of C(23, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_23_3_degree_pos : 0 < luebeckConwayPolynomial_23_3.degree

Positive degree of C(23, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_23_3 : luebeckConwayPolynomial? 23 3 = some luebeckConwayPolynomial_23_3

Lookup identifies the imported C(23, 3).

def Hex.Conway.luebeckConwayPolynomial_41_3 : FpPoly 41

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_41_3_monic : DensePoly.Monic luebeckConwayPolynomial_41_3

Monicity of C(41, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_41_3_degree_pos : 0 < luebeckConwayPolynomial_41_3.degree

Positive degree of C(41, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_41_3 : luebeckConwayPolynomial? 41 3 = some luebeckConwayPolynomial_41_3

Lookup identifies the imported C(41, 3).

def Hex.Conway.luebeckConwayPolynomial_571_2 : FpPoly 571

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_571_2_monic : DensePoly.Monic luebeckConwayPolynomial_571_2

Monicity of C(571, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_571_2_degree_pos : 0 < luebeckConwayPolynomial_571_2.degree

Positive degree of C(571, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_571_2 : luebeckConwayPolynomial? 571 2 = some luebeckConwayPolynomial_571_2

Lookup identifies the imported C(571, 2).

def Hex.Conway.luebeckConwayPolynomial_911_2 : FpPoly 911

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_911_2_monic : DensePoly.Monic luebeckConwayPolynomial_911_2

Monicity of C(911, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_911_2_degree_pos : 0 < luebeckConwayPolynomial_911_2.degree

Positive degree of C(911, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_911_2 : luebeckConwayPolynomial? 911 2 = some luebeckConwayPolynomial_911_2

Lookup identifies the imported C(911, 2).

def Hex.Conway.luebeckConwayPolynomial_569_2 : FpPoly 569

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_569_2_monic : DensePoly.Monic luebeckConwayPolynomial_569_2

Monicity of C(569, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_569_2_degree_pos : 0 < luebeckConwayPolynomial_569_2.degree

Positive degree of C(569, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_569_2 : luebeckConwayPolynomial? 569 2 = some luebeckConwayPolynomial_569_2

Lookup identifies the imported C(569, 2).

def Hex.Conway.luebeckConwayPolynomial_619_2 : FpPoly 619

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_619_2_monic : DensePoly.Monic luebeckConwayPolynomial_619_2

Monicity of C(619, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_619_2_degree_pos : 0 < luebeckConwayPolynomial_619_2.degree

Positive degree of C(619, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_619_2 : luebeckConwayPolynomial? 619 2 = some luebeckConwayPolynomial_619_2

Lookup identifies the imported C(619, 2).

def Hex.Conway.luebeckConwayPolynomial_683_2 : FpPoly 683

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_683_2_monic : DensePoly.Monic luebeckConwayPolynomial_683_2

Monicity of C(683, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_683_2_degree_pos : 0 < luebeckConwayPolynomial_683_2.degree

Positive degree of C(683, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_683_2 : luebeckConwayPolynomial? 683 2 = some luebeckConwayPolynomial_683_2

Lookup identifies the imported C(683, 2).

def Hex.Conway.luebeckConwayPolynomial_727_2 : FpPoly 727

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_727_2_monic : DensePoly.Monic luebeckConwayPolynomial_727_2

Monicity of C(727, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_727_2_degree_pos : 0 < luebeckConwayPolynomial_727_2.degree

Positive degree of C(727, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_727_2 : luebeckConwayPolynomial? 727 2 = some luebeckConwayPolynomial_727_2

Lookup identifies the imported C(727, 2).

def Hex.Conway.luebeckConwayPolynomial_769_2 : FpPoly 769

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

Equations

• Hex.Conway.luebeckConwayPolynomial_769_2 = { coeffs := #[11, 765, 1], normalized := Hex.Conway.luebeckConwayPolynomial_769_2._proof_1 }

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_769_2_monic : DensePoly.Monic luebeckConwayPolynomial_769_2

Monicity of C(769, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_769_2_degree_pos : 0 < luebeckConwayPolynomial_769_2.degree

Positive degree of C(769, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_769_2 : luebeckConwayPolynomial? 769 2 = some luebeckConwayPolynomial_769_2

Lookup identifies the imported C(769, 2).

def Hex.Conway.luebeckConwayPolynomial_827_2 : FpPoly 827

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_827_2_monic : DensePoly.Monic luebeckConwayPolynomial_827_2

Monicity of C(827, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_827_2_degree_pos : 0 < luebeckConwayPolynomial_827_2.degree

Positive degree of C(827, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_827_2 : luebeckConwayPolynomial? 827 2 = some luebeckConwayPolynomial_827_2

Lookup identifies the imported C(827, 2).

def Hex.Conway.luebeckConwayPolynomial_857_2 : FpPoly 857

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_857_2_monic : DensePoly.Monic luebeckConwayPolynomial_857_2

Monicity of C(857, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_857_2_degree_pos : 0 < luebeckConwayPolynomial_857_2.degree

Positive degree of C(857, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_857_2 : luebeckConwayPolynomial? 857 2 = some luebeckConwayPolynomial_857_2

Lookup identifies the imported C(857, 2).