def Hex.Conway.luebeckConwayPolynomial_257_2 : FpPoly 257

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_257_2_monic : DensePoly.Monic luebeckConwayPolynomial_257_2

Monicity of C(257, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_257_2_degree_pos : 0 < luebeckConwayPolynomial_257_2.degree

Positive degree of C(257, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_257_2 : luebeckConwayPolynomial? 257 2 = some luebeckConwayPolynomial_257_2

Lookup identifies the imported C(257, 2).

def Hex.Conway.luebeckConwayPolynomial_487_2 : FpPoly 487

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_487_2_monic : DensePoly.Monic luebeckConwayPolynomial_487_2

Monicity of C(487, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_487_2_degree_pos : 0 < luebeckConwayPolynomial_487_2.degree

Positive degree of C(487, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_487_2 : luebeckConwayPolynomial? 487 2 = some luebeckConwayPolynomial_487_2

Lookup identifies the imported C(487, 2).

def Hex.Conway.luebeckConwayPolynomial_73_2 : FpPoly 73

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_73_2_monic : DensePoly.Monic luebeckConwayPolynomial_73_2

Monicity of C(73, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_73_2_degree_pos : 0 < luebeckConwayPolynomial_73_2.degree

Positive degree of C(73, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_73_2 : luebeckConwayPolynomial? 73 2 = some luebeckConwayPolynomial_73_2

Lookup identifies the imported C(73, 2).

def Hex.Conway.luebeckConwayPolynomial_97_2 : FpPoly 97

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_97_2_monic : DensePoly.Monic luebeckConwayPolynomial_97_2

Monicity of C(97, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_97_2_degree_pos : 0 < luebeckConwayPolynomial_97_2.degree

Positive degree of C(97, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_97_2 : luebeckConwayPolynomial? 97 2 = some luebeckConwayPolynomial_97_2

Lookup identifies the imported C(97, 2).

def Hex.Conway.luebeckConwayPolynomial_29_2 : FpPoly 29

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_29_2_monic : DensePoly.Monic luebeckConwayPolynomial_29_2

Monicity of C(29, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_29_2_degree_pos : 0 < luebeckConwayPolynomial_29_2.degree

Positive degree of C(29, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_29_2 : luebeckConwayPolynomial? 29 2 = some luebeckConwayPolynomial_29_2

Lookup identifies the imported C(29, 2).

def Hex.Conway.luebeckConwayPolynomial_3_3 : FpPoly 3

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_3_3_monic : DensePoly.Monic luebeckConwayPolynomial_3_3

Monicity of C(3, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_3_3_degree_pos : 0 < luebeckConwayPolynomial_3_3.degree

Positive degree of C(3, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_3_3 : luebeckConwayPolynomial? 3 3 = some luebeckConwayPolynomial_3_3

Lookup identifies the imported C(3, 3).

def Hex.Conway.luebeckConwayPolynomial_17_2 : FpPoly 17

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_17_2_monic : DensePoly.Monic luebeckConwayPolynomial_17_2

Monicity of C(17, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_17_2_degree_pos : 0 < luebeckConwayPolynomial_17_2.degree

Positive degree of C(17, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_17_2 : luebeckConwayPolynomial? 17 2 = some luebeckConwayPolynomial_17_2

Lookup identifies the imported C(17, 2).

def Hex.Conway.luebeckConwayPolynomial_7_2 : FpPoly 7

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_7_2_monic : DensePoly.Monic luebeckConwayPolynomial_7_2

Monicity of C(7, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_7_2_degree_pos : 0 < luebeckConwayPolynomial_7_2.degree

Positive degree of C(7, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_7_2 : luebeckConwayPolynomial? 7 2 = some luebeckConwayPolynomial_7_2

Lookup identifies the imported C(7, 2).

def Hex.Conway.luebeckConwayPolynomial_661_1 : FpPoly 661

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

Equations

• Hex.Conway.luebeckConwayPolynomial_661_1 = { coeffs := #[659, 1], normalized := Hex.Conway.luebeckConwayPolynomial_661_1._proof_1 }

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_661_1_monic : DensePoly.Monic luebeckConwayPolynomial_661_1

Monicity of C(661, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_661_1_degree_pos : 0 < luebeckConwayPolynomial_661_1.degree

Positive degree of C(661, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_661_1 : luebeckConwayPolynomial? 661 1 = some luebeckConwayPolynomial_661_1

Lookup identifies the imported C(661, 1).

def Hex.Conway.luebeckConwayPolynomial_967_1 : FpPoly 967

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

Equations

• Hex.Conway.luebeckConwayPolynomial_967_1 = { coeffs := #[962, 1], normalized := Hex.Conway.luebeckConwayPolynomial_967_1._proof_1 }

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_967_1_monic : DensePoly.Monic luebeckConwayPolynomial_967_1

Monicity of C(967, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_967_1_degree_pos : 0 < luebeckConwayPolynomial_967_1.degree

Positive degree of C(967, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_967_1 : luebeckConwayPolynomial? 967 1 = some luebeckConwayPolynomial_967_1

Lookup identifies the imported C(967, 1).

def Hex.Conway.luebeckConwayPolynomial_463_1 : FpPoly 463

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

Equations

• Hex.Conway.luebeckConwayPolynomial_463_1 = { coeffs := #[460, 1], normalized := Hex.Conway.luebeckConwayPolynomial_463_1._proof_1 }

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_463_1_monic : DensePoly.Monic luebeckConwayPolynomial_463_1

Monicity of C(463, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_463_1_degree_pos : 0 < luebeckConwayPolynomial_463_1.degree

Positive degree of C(463, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_463_1 : luebeckConwayPolynomial? 463 1 = some luebeckConwayPolynomial_463_1

Lookup identifies the imported C(463, 1).

def Hex.Conway.luebeckConwayPolynomial_601_1 : FpPoly 601

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_601_1_monic : DensePoly.Monic luebeckConwayPolynomial_601_1

Monicity of C(601, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_601_1_degree_pos : 0 < luebeckConwayPolynomial_601_1.degree

Positive degree of C(601, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_601_1 : luebeckConwayPolynomial? 601 1 = some luebeckConwayPolynomial_601_1

Lookup identifies the imported C(601, 1).

def Hex.Conway.luebeckConwayPolynomial_619_1 : FpPoly 619

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_619_1_monic : DensePoly.Monic luebeckConwayPolynomial_619_1

Monicity of C(619, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_619_1_degree_pos : 0 < luebeckConwayPolynomial_619_1.degree

Positive degree of C(619, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_619_1 : luebeckConwayPolynomial? 619 1 = some luebeckConwayPolynomial_619_1

Lookup identifies the imported C(619, 1).

def Hex.Conway.luebeckConwayPolynomial_673_1 : FpPoly 673

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

Equations

• Hex.Conway.luebeckConwayPolynomial_673_1 = { coeffs := #[668, 1], normalized := Hex.Conway.luebeckConwayPolynomial_673_1._proof_1 }

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_673_1_monic : DensePoly.Monic luebeckConwayPolynomial_673_1

Monicity of C(673, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_673_1_degree_pos : 0 < luebeckConwayPolynomial_673_1.degree

Positive degree of C(673, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_673_1 : luebeckConwayPolynomial? 673 1 = some luebeckConwayPolynomial_673_1

Lookup identifies the imported C(673, 1).

def Hex.Conway.luebeckConwayPolynomial_727_1 : FpPoly 727

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

Equations

• Hex.Conway.luebeckConwayPolynomial_727_1 = { coeffs := #[722, 1], normalized := Hex.Conway.luebeckConwayPolynomial_727_1._proof_1 }

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_727_1_monic : DensePoly.Monic luebeckConwayPolynomial_727_1

Monicity of C(727, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_727_1_degree_pos : 0 < luebeckConwayPolynomial_727_1.degree

Positive degree of C(727, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_727_1 : luebeckConwayPolynomial? 727 1 = some luebeckConwayPolynomial_727_1

Lookup identifies the imported C(727, 1).

def Hex.Conway.luebeckConwayPolynomial_751_1 : FpPoly 751

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

Equations

• Hex.Conway.luebeckConwayPolynomial_751_1 = { coeffs := #[748, 1], normalized := Hex.Conway.luebeckConwayPolynomial_751_1._proof_1 }

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_751_1_monic : DensePoly.Monic luebeckConwayPolynomial_751_1

Monicity of C(751, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_751_1_degree_pos : 0 < luebeckConwayPolynomial_751_1.degree

Positive degree of C(751, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_751_1 : luebeckConwayPolynomial? 751 1 = some luebeckConwayPolynomial_751_1

Lookup identifies the imported C(751, 1).

def Hex.Conway.luebeckConwayPolynomial_811_1 : FpPoly 811

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

Equations

• Hex.Conway.luebeckConwayPolynomial_811_1 = { coeffs := #[808, 1], normalized := Hex.Conway.luebeckConwayPolynomial_811_1._proof_1 }

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_811_1_monic : DensePoly.Monic luebeckConwayPolynomial_811_1

Monicity of C(811, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_811_1_degree_pos : 0 < luebeckConwayPolynomial_811_1.degree

Positive degree of C(811, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_811_1 : luebeckConwayPolynomial? 811 1 = some luebeckConwayPolynomial_811_1

Lookup identifies the imported C(811, 1).

def Hex.Conway.luebeckConwayPolynomial_829_1 : FpPoly 829

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

Equations

• Hex.Conway.luebeckConwayPolynomial_829_1 = { coeffs := #[827, 1], normalized := Hex.Conway.luebeckConwayPolynomial_829_1._proof_1 }

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_829_1_monic : DensePoly.Monic luebeckConwayPolynomial_829_1

Monicity of C(829, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_829_1_degree_pos : 0 < luebeckConwayPolynomial_829_1.degree

Positive degree of C(829, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_829_1 : luebeckConwayPolynomial? 829 1 = some luebeckConwayPolynomial_829_1

Lookup identifies the imported C(829, 1).

def Hex.Conway.luebeckConwayPolynomial_883_1 : FpPoly 883

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

Equations

• Hex.Conway.luebeckConwayPolynomial_883_1 = { coeffs := #[881, 1], normalized := Hex.Conway.luebeckConwayPolynomial_883_1._proof_1 }

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_883_1_monic : DensePoly.Monic luebeckConwayPolynomial_883_1

Monicity of C(883, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_883_1_degree_pos : 0 < luebeckConwayPolynomial_883_1.degree

Positive degree of C(883, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_883_1 : luebeckConwayPolynomial? 883 1 = some luebeckConwayPolynomial_883_1

Lookup identifies the imported C(883, 1).

def Hex.Conway.luebeckConwayPolynomial_941_1 : FpPoly 941

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

Equations

• Hex.Conway.luebeckConwayPolynomial_941_1 = { coeffs := #[939, 1], normalized := Hex.Conway.luebeckConwayPolynomial_941_1._proof_1 }

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_941_1_monic : DensePoly.Monic luebeckConwayPolynomial_941_1

Monicity of C(941, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_941_1_degree_pos : 0 < luebeckConwayPolynomial_941_1.degree

Positive degree of C(941, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_941_1 : luebeckConwayPolynomial? 941 1 = some luebeckConwayPolynomial_941_1

Lookup identifies the imported C(941, 1).

def Hex.Conway.luebeckConwayPolynomial_997_1 : FpPoly 997

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

Equations

• Hex.Conway.luebeckConwayPolynomial_997_1 = { coeffs := #[990, 1], normalized := Hex.Conway.luebeckConwayPolynomial_997_1._proof_1 }

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_997_1_monic : DensePoly.Monic luebeckConwayPolynomial_997_1

Monicity of C(997, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_997_1_degree_pos : 0 < luebeckConwayPolynomial_997_1.degree

Positive degree of C(997, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_997_1 : luebeckConwayPolynomial? 997 1 = some luebeckConwayPolynomial_997_1

Lookup identifies the imported C(997, 1).

def Hex.Conway.luebeckConwayPolynomial_283_1 : FpPoly 283

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_283_1_monic : DensePoly.Monic luebeckConwayPolynomial_283_1

Monicity of C(283, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_283_1_degree_pos : 0 < luebeckConwayPolynomial_283_1.degree

Positive degree of C(283, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_283_1 : luebeckConwayPolynomial? 283 1 = some luebeckConwayPolynomial_283_1

Lookup identifies the imported C(283, 1).

def Hex.Conway.luebeckConwayPolynomial_337_1 : FpPoly 337

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

Equations

• Hex.Conway.luebeckConwayPolynomial_337_1 = { coeffs := #[327, 1], normalized := Hex.Conway.luebeckConwayPolynomial_337_1._proof_1 }

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_337_1_monic : DensePoly.Monic luebeckConwayPolynomial_337_1

Monicity of C(337, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_337_1_degree_pos : 0 < luebeckConwayPolynomial_337_1.degree

Positive degree of C(337, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_337_1 : luebeckConwayPolynomial? 337 1 = some luebeckConwayPolynomial_337_1

Lookup identifies the imported C(337, 1).

def Hex.Conway.luebeckConwayPolynomial_379_1 : FpPoly 379

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_379_1_monic : DensePoly.Monic luebeckConwayPolynomial_379_1

Monicity of C(379, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_379_1_degree_pos : 0 < luebeckConwayPolynomial_379_1.degree

Positive degree of C(379, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_379_1 : luebeckConwayPolynomial? 379 1 = some luebeckConwayPolynomial_379_1

Lookup identifies the imported C(379, 1).