def Hex.Conway.luebeckConwayPolynomial_281_1 : FpPoly 281

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_281_1_monic : DensePoly.Monic luebeckConwayPolynomial_281_1

Monicity of C(281, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_281_1_degree_pos : 0 < luebeckConwayPolynomial_281_1.degree

Positive degree of C(281, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_281_1 : luebeckConwayPolynomial? 281 1 = some luebeckConwayPolynomial_281_1

Lookup identifies the imported C(281, 1).

def Hex.Conway.luebeckConwayPolynomial_313_1 : FpPoly 313

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_313_1_monic : DensePoly.Monic luebeckConwayPolynomial_313_1

Monicity of C(313, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_313_1_degree_pos : 0 < luebeckConwayPolynomial_313_1.degree

Positive degree of C(313, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_313_1 : luebeckConwayPolynomial? 313 1 = some luebeckConwayPolynomial_313_1

Lookup identifies the imported C(313, 1).

def Hex.Conway.luebeckConwayPolynomial_373_1 : FpPoly 373

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_373_1_monic : DensePoly.Monic luebeckConwayPolynomial_373_1

Monicity of C(373, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_373_1_degree_pos : 0 < luebeckConwayPolynomial_373_1.degree

Positive degree of C(373, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_373_1 : luebeckConwayPolynomial? 373 1 = some luebeckConwayPolynomial_373_1

Lookup identifies the imported C(373, 1).

def Hex.Conway.luebeckConwayPolynomial_419_1 : FpPoly 419

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_419_1_monic : DensePoly.Monic luebeckConwayPolynomial_419_1

Monicity of C(419, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_419_1_degree_pos : 0 < luebeckConwayPolynomial_419_1.degree

Positive degree of C(419, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_419_1 : luebeckConwayPolynomial? 419 1 = some luebeckConwayPolynomial_419_1

Lookup identifies the imported C(419, 1).

def Hex.Conway.luebeckConwayPolynomial_457_1 : FpPoly 457

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_457_1_monic : DensePoly.Monic luebeckConwayPolynomial_457_1

Monicity of C(457, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_457_1_degree_pos : 0 < luebeckConwayPolynomial_457_1.degree

Positive degree of C(457, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_457_1 : luebeckConwayPolynomial? 457 1 = some luebeckConwayPolynomial_457_1

Lookup identifies the imported C(457, 1).

def Hex.Conway.luebeckConwayPolynomial_131_1 : FpPoly 131

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_131_1_monic : DensePoly.Monic luebeckConwayPolynomial_131_1

Monicity of C(131, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_131_1_degree_pos : 0 < luebeckConwayPolynomial_131_1.degree

Positive degree of C(131, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_131_1 : luebeckConwayPolynomial? 131 1 = some luebeckConwayPolynomial_131_1

Lookup identifies the imported C(131, 1).

def Hex.Conway.luebeckConwayPolynomial_157_1 : FpPoly 157

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_157_1_monic : DensePoly.Monic luebeckConwayPolynomial_157_1

Monicity of C(157, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_157_1_degree_pos : 0 < luebeckConwayPolynomial_157_1.degree

Positive degree of C(157, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_157_1 : luebeckConwayPolynomial? 157 1 = some luebeckConwayPolynomial_157_1

Lookup identifies the imported C(157, 1).

def Hex.Conway.luebeckConwayPolynomial_223_1 : FpPoly 223

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_223_1_monic : DensePoly.Monic luebeckConwayPolynomial_223_1

Monicity of C(223, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_223_1_degree_pos : 0 < luebeckConwayPolynomial_223_1.degree

Positive degree of C(223, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_223_1 : luebeckConwayPolynomial? 223 1 = some luebeckConwayPolynomial_223_1

Lookup identifies the imported C(223, 1).

def Hex.Conway.luebeckConwayPolynomial_67_1 : FpPoly 67

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_67_1_monic : DensePoly.Monic luebeckConwayPolynomial_67_1

Monicity of C(67, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_67_1_degree_pos : 0 < luebeckConwayPolynomial_67_1.degree

Positive degree of C(67, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_67_1 : luebeckConwayPolynomial? 67 1 = some luebeckConwayPolynomial_67_1

Lookup identifies the imported C(67, 1).

def Hex.Conway.luebeckConwayPolynomial_127_1 : FpPoly 127

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_127_1_monic : DensePoly.Monic luebeckConwayPolynomial_127_1

Monicity of C(127, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_127_1_degree_pos : 0 < luebeckConwayPolynomial_127_1.degree

Positive degree of C(127, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_127_1 : luebeckConwayPolynomial? 127 1 = some luebeckConwayPolynomial_127_1

Lookup identifies the imported C(127, 1).

def Hex.Conway.luebeckConwayPolynomial_587_1 : FpPoly 587

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_587_1_monic : DensePoly.Monic luebeckConwayPolynomial_587_1

Monicity of C(587, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_587_1_degree_pos : 0 < luebeckConwayPolynomial_587_1.degree

Positive degree of C(587, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_587_1 : luebeckConwayPolynomial? 587 1 = some luebeckConwayPolynomial_587_1

Lookup identifies the imported C(587, 1).

def Hex.Conway.luebeckConwayPolynomial_677_1 : FpPoly 677

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_677_1_monic : DensePoly.Monic luebeckConwayPolynomial_677_1

Monicity of C(677, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_677_1_degree_pos : 0 < luebeckConwayPolynomial_677_1.degree

Positive degree of C(677, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_677_1 : luebeckConwayPolynomial? 677 1 = some luebeckConwayPolynomial_677_1

Lookup identifies the imported C(677, 1).

def Hex.Conway.luebeckConwayPolynomial_797_1 : FpPoly 797

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_797_1_monic : DensePoly.Monic luebeckConwayPolynomial_797_1

Monicity of C(797, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_797_1_degree_pos : 0 < luebeckConwayPolynomial_797_1.degree

Positive degree of C(797, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_797_1 : luebeckConwayPolynomial? 797 1 = some luebeckConwayPolynomial_797_1

Lookup identifies the imported C(797, 1).

def Hex.Conway.luebeckConwayPolynomial_863_1 : FpPoly 863

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_863_1_monic : DensePoly.Monic luebeckConwayPolynomial_863_1

Monicity of C(863, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_863_1_degree_pos : 0 < luebeckConwayPolynomial_863_1.degree

Positive degree of C(863, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_863_1 : luebeckConwayPolynomial? 863 1 = some luebeckConwayPolynomial_863_1

Lookup identifies the imported C(863, 1).

def Hex.Conway.luebeckConwayPolynomial_983_1 : FpPoly 983

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_983_1_monic : DensePoly.Monic luebeckConwayPolynomial_983_1

Monicity of C(983, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_983_1_degree_pos : 0 < luebeckConwayPolynomial_983_1.degree

Positive degree of C(983, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_983_1 : luebeckConwayPolynomial? 983 1 = some luebeckConwayPolynomial_983_1

Lookup identifies the imported C(983, 1).

def Hex.Conway.luebeckConwayPolynomial_293_1 : FpPoly 293

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_293_1_monic : DensePoly.Monic luebeckConwayPolynomial_293_1

Monicity of C(293, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_293_1_degree_pos : 0 < luebeckConwayPolynomial_293_1.degree

Positive degree of C(293, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_293_1 : luebeckConwayPolynomial? 293 1 = some luebeckConwayPolynomial_293_1

Lookup identifies the imported C(293, 1).

def Hex.Conway.luebeckConwayPolynomial_359_1 : FpPoly 359

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_359_1_monic : DensePoly.Monic luebeckConwayPolynomial_359_1

Monicity of C(359, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_359_1_degree_pos : 0 < luebeckConwayPolynomial_359_1.degree

Positive degree of C(359, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_359_1 : luebeckConwayPolynomial? 359 1 = some luebeckConwayPolynomial_359_1

Lookup identifies the imported C(359, 1).

def Hex.Conway.luebeckConwayPolynomial_433_1 : FpPoly 433

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_433_1_monic : DensePoly.Monic luebeckConwayPolynomial_433_1

Monicity of C(433, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_433_1_degree_pos : 0 < luebeckConwayPolynomial_433_1.degree

Positive degree of C(433, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_433_1 : luebeckConwayPolynomial? 433 1 = some luebeckConwayPolynomial_433_1

Lookup identifies the imported C(433, 1).

def Hex.Conway.luebeckConwayPolynomial_487_1 : FpPoly 487

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_487_1_monic : DensePoly.Monic luebeckConwayPolynomial_487_1

Monicity of C(487, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_487_1_degree_pos : 0 < luebeckConwayPolynomial_487_1.degree

Positive degree of C(487, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_487_1 : luebeckConwayPolynomial? 487 1 = some luebeckConwayPolynomial_487_1

Lookup identifies the imported C(487, 1).

def Hex.Conway.luebeckConwayPolynomial_3_2 : FpPoly 3

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_3_2_monic : DensePoly.Monic luebeckConwayPolynomial_3_2

Monicity of C(3, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_3_2_degree_pos : 0 < luebeckConwayPolynomial_3_2.degree

Positive degree of C(3, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_3_2 : luebeckConwayPolynomial? 3 2 = some luebeckConwayPolynomial_3_2

Lookup identifies the imported C(3, 2).

def Hex.Conway.luebeckConwayPolynomial_163_1 : FpPoly 163

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_163_1_monic : DensePoly.Monic luebeckConwayPolynomial_163_1

Monicity of C(163, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_163_1_degree_pos : 0 < luebeckConwayPolynomial_163_1.degree

Positive degree of C(163, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_163_1 : luebeckConwayPolynomial? 163 1 = some luebeckConwayPolynomial_163_1

Lookup identifies the imported C(163, 1).

def Hex.Conway.luebeckConwayPolynomial_193_1 : FpPoly 193

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_193_1_monic : DensePoly.Monic luebeckConwayPolynomial_193_1

Monicity of C(193, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_193_1_degree_pos : 0 < luebeckConwayPolynomial_193_1.degree

Positive degree of C(193, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_193_1 : luebeckConwayPolynomial? 193 1 = some luebeckConwayPolynomial_193_1

Lookup identifies the imported C(193, 1).

def Hex.Conway.luebeckConwayPolynomial_251_1 : FpPoly 251

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_251_1_monic : DensePoly.Monic luebeckConwayPolynomial_251_1

Monicity of C(251, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_251_1_degree_pos : 0 < luebeckConwayPolynomial_251_1.degree

Positive degree of C(251, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_251_1 : luebeckConwayPolynomial? 251 1 = some luebeckConwayPolynomial_251_1

Lookup identifies the imported C(251, 1).

def Hex.Conway.luebeckConwayPolynomial_97_1 : FpPoly 97

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_97_1_monic : DensePoly.Monic luebeckConwayPolynomial_97_1

Monicity of C(97, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_97_1_degree_pos : 0 < luebeckConwayPolynomial_97_1.degree

Positive degree of C(97, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_97_1 : luebeckConwayPolynomial? 97 1 = some luebeckConwayPolynomial_97_1

Lookup identifies the imported C(97, 1).