def Hex.Conway.luebeckConwayPolynomial_947_1 : FpPoly 947

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_947_1_monic : DensePoly.Monic luebeckConwayPolynomial_947_1

Monicity of C(947, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_947_1_degree_pos : 0 < luebeckConwayPolynomial_947_1.degree

Positive degree of C(947, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_947_1 : luebeckConwayPolynomial? 947 1 = some luebeckConwayPolynomial_947_1

Lookup identifies the imported C(947, 1).

def Hex.Conway.luebeckConwayPolynomial_271_1 : FpPoly 271

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_271_1_monic : DensePoly.Monic luebeckConwayPolynomial_271_1

Monicity of C(271, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_271_1_degree_pos : 0 < luebeckConwayPolynomial_271_1.degree

Positive degree of C(271, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_271_1 : luebeckConwayPolynomial? 271 1 = some luebeckConwayPolynomial_271_1

Lookup identifies the imported C(271, 1).

def Hex.Conway.luebeckConwayPolynomial_307_1 : FpPoly 307

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_307_1_monic : DensePoly.Monic luebeckConwayPolynomial_307_1

Monicity of C(307, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_307_1_degree_pos : 0 < luebeckConwayPolynomial_307_1.degree

Positive degree of C(307, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_307_1 : luebeckConwayPolynomial? 307 1 = some luebeckConwayPolynomial_307_1

Lookup identifies the imported C(307, 1).

def Hex.Conway.luebeckConwayPolynomial_349_1 : FpPoly 349

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_349_1_monic : DensePoly.Monic luebeckConwayPolynomial_349_1

Monicity of C(349, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_349_1_degree_pos : 0 < luebeckConwayPolynomial_349_1.degree

Positive degree of C(349, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_349_1 : luebeckConwayPolynomial? 349 1 = some luebeckConwayPolynomial_349_1

Lookup identifies the imported C(349, 1).

def Hex.Conway.luebeckConwayPolynomial_397_1 : FpPoly 397

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_397_1_monic : DensePoly.Monic luebeckConwayPolynomial_397_1

Monicity of C(397, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_397_1_degree_pos : 0 < luebeckConwayPolynomial_397_1.degree

Positive degree of C(397, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_397_1 : luebeckConwayPolynomial? 397 1 = some luebeckConwayPolynomial_397_1

Lookup identifies the imported C(397, 1).

def Hex.Conway.luebeckConwayPolynomial_439_1 : FpPoly 439

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_439_1_monic : DensePoly.Monic luebeckConwayPolynomial_439_1

Monicity of C(439, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_439_1_degree_pos : 0 < luebeckConwayPolynomial_439_1.degree

Positive degree of C(439, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_439_1 : luebeckConwayPolynomial? 439 1 = some luebeckConwayPolynomial_439_1

Lookup identifies the imported C(439, 1).

def Hex.Conway.luebeckConwayPolynomial_491_1 : FpPoly 491

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_491_1_monic : DensePoly.Monic luebeckConwayPolynomial_491_1

Monicity of C(491, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_491_1_degree_pos : 0 < luebeckConwayPolynomial_491_1.degree

Positive degree of C(491, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_491_1 : luebeckConwayPolynomial? 491 1 = some luebeckConwayPolynomial_491_1

Lookup identifies the imported C(491, 1).

def Hex.Conway.luebeckConwayPolynomial_151_1 : FpPoly 151

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_151_1_monic : DensePoly.Monic luebeckConwayPolynomial_151_1

Monicity of C(151, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_151_1_degree_pos : 0 < luebeckConwayPolynomial_151_1.degree

Positive degree of C(151, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_151_1 : luebeckConwayPolynomial? 151 1 = some luebeckConwayPolynomial_151_1

Lookup identifies the imported C(151, 1).

def Hex.Conway.luebeckConwayPolynomial_199_1 : FpPoly 199

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_199_1_monic : DensePoly.Monic luebeckConwayPolynomial_199_1

Monicity of C(199, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_199_1_degree_pos : 0 < luebeckConwayPolynomial_199_1.degree

Positive degree of C(199, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_199_1 : luebeckConwayPolynomial? 199 1 = some luebeckConwayPolynomial_199_1

Lookup identifies the imported C(199, 1).

def Hex.Conway.luebeckConwayPolynomial_241_1 : FpPoly 241

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_241_1_monic : DensePoly.Monic luebeckConwayPolynomial_241_1

Monicity of C(241, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_241_1_degree_pos : 0 < luebeckConwayPolynomial_241_1.degree

Positive degree of C(241, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_241_1 : luebeckConwayPolynomial? 241 1 = some luebeckConwayPolynomial_241_1

Lookup identifies the imported C(241, 1).

def Hex.Conway.luebeckConwayPolynomial_103_1 : FpPoly 103

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_103_1_monic : DensePoly.Monic luebeckConwayPolynomial_103_1

Monicity of C(103, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_103_1_degree_pos : 0 < luebeckConwayPolynomial_103_1.degree

Positive degree of C(103, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_103_1 : luebeckConwayPolynomial? 103 1 = some luebeckConwayPolynomial_103_1

Lookup identifies the imported C(103, 1).

def Hex.Conway.luebeckConwayPolynomial_569_1 : FpPoly 569

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_569_1_monic : DensePoly.Monic luebeckConwayPolynomial_569_1

Monicity of C(569, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_569_1_degree_pos : 0 < luebeckConwayPolynomial_569_1.degree

Positive degree of C(569, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_569_1 : luebeckConwayPolynomial? 569 1 = some luebeckConwayPolynomial_569_1

Lookup identifies the imported C(569, 1).

def Hex.Conway.luebeckConwayPolynomial_641_1 : FpPoly 641

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_641_1_monic : DensePoly.Monic luebeckConwayPolynomial_641_1

Monicity of C(641, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_641_1_degree_pos : 0 < luebeckConwayPolynomial_641_1.degree

Positive degree of C(641, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_641_1 : luebeckConwayPolynomial? 641 1 = some luebeckConwayPolynomial_641_1

Lookup identifies the imported C(641, 1).

def Hex.Conway.luebeckConwayPolynomial_769_1 : FpPoly 769

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_769_1_monic : DensePoly.Monic luebeckConwayPolynomial_769_1

Monicity of C(769, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_769_1_degree_pos : 0 < luebeckConwayPolynomial_769_1.degree

Positive degree of C(769, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_769_1 : luebeckConwayPolynomial? 769 1 = some luebeckConwayPolynomial_769_1

Lookup identifies the imported C(769, 1).

def Hex.Conway.luebeckConwayPolynomial_839_1 : FpPoly 839

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_839_1_monic : DensePoly.Monic luebeckConwayPolynomial_839_1

Monicity of C(839, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_839_1_degree_pos : 0 < luebeckConwayPolynomial_839_1.degree

Positive degree of C(839, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_839_1 : luebeckConwayPolynomial? 839 1 = some luebeckConwayPolynomial_839_1

Lookup identifies the imported C(839, 1).

def Hex.Conway.luebeckConwayPolynomial_929_1 : FpPoly 929

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_929_1_monic : DensePoly.Monic luebeckConwayPolynomial_929_1

Monicity of C(929, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_929_1_degree_pos : 0 < luebeckConwayPolynomial_929_1.degree

Positive degree of C(929, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_929_1 : luebeckConwayPolynomial? 929 1 = some luebeckConwayPolynomial_929_1

Lookup identifies the imported C(929, 1).

def Hex.Conway.luebeckConwayPolynomial_61_1 : FpPoly 61

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_61_1_monic : DensePoly.Monic luebeckConwayPolynomial_61_1

Monicity of C(61, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_61_1_degree_pos : 0 < luebeckConwayPolynomial_61_1.degree

Positive degree of C(61, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_61_1 : luebeckConwayPolynomial? 61 1 = some luebeckConwayPolynomial_61_1

Lookup identifies the imported C(61, 1).

def Hex.Conway.luebeckConwayPolynomial_317_1 : FpPoly 317

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_317_1_monic : DensePoly.Monic luebeckConwayPolynomial_317_1

Monicity of C(317, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_317_1_degree_pos : 0 < luebeckConwayPolynomial_317_1.degree

Positive degree of C(317, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_317_1 : luebeckConwayPolynomial? 317 1 = some luebeckConwayPolynomial_317_1

Lookup identifies the imported C(317, 1).

def Hex.Conway.luebeckConwayPolynomial_383_1 : FpPoly 383

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_383_1_monic : DensePoly.Monic luebeckConwayPolynomial_383_1

Monicity of C(383, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_383_1_degree_pos : 0 < luebeckConwayPolynomial_383_1.degree

Positive degree of C(383, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_383_1 : luebeckConwayPolynomial? 383 1 = some luebeckConwayPolynomial_383_1

Lookup identifies the imported C(383, 1).

def Hex.Conway.luebeckConwayPolynomial_449_1 : FpPoly 449

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_449_1_monic : DensePoly.Monic luebeckConwayPolynomial_449_1

Monicity of C(449, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_449_1_degree_pos : 0 < luebeckConwayPolynomial_449_1.degree

Positive degree of C(449, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_449_1 : luebeckConwayPolynomial? 449 1 = some luebeckConwayPolynomial_449_1

Lookup identifies the imported C(449, 1).

def Hex.Conway.luebeckConwayPolynomial_503_1 : FpPoly 503

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_503_1_monic : DensePoly.Monic luebeckConwayPolynomial_503_1

Monicity of C(503, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_503_1_degree_pos : 0 < luebeckConwayPolynomial_503_1.degree

Positive degree of C(503, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_503_1 : luebeckConwayPolynomial? 503 1 = some luebeckConwayPolynomial_503_1

Lookup identifies the imported C(503, 1).

def Hex.Conway.luebeckConwayPolynomial_137_1 : FpPoly 137

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_137_1_monic : DensePoly.Monic luebeckConwayPolynomial_137_1

Monicity of C(137, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_137_1_degree_pos : 0 < luebeckConwayPolynomial_137_1.degree

Positive degree of C(137, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_137_1 : luebeckConwayPolynomial? 137 1 = some luebeckConwayPolynomial_137_1

Lookup identifies the imported C(137, 1).

def Hex.Conway.luebeckConwayPolynomial_173_1 : FpPoly 173

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_173_1_monic : DensePoly.Monic luebeckConwayPolynomial_173_1

Monicity of C(173, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_173_1_degree_pos : 0 < luebeckConwayPolynomial_173_1.degree

Positive degree of C(173, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_173_1 : luebeckConwayPolynomial? 173 1 = some luebeckConwayPolynomial_173_1

Lookup identifies the imported C(173, 1).

def Hex.Conway.luebeckConwayPolynomial_227_1 : FpPoly 227

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_227_1_monic : DensePoly.Monic luebeckConwayPolynomial_227_1

Monicity of C(227, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_227_1_degree_pos : 0 < luebeckConwayPolynomial_227_1.degree

Positive degree of C(227, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_227_1 : luebeckConwayPolynomial? 227 1 = some luebeckConwayPolynomial_227_1

Lookup identifies the imported C(227, 1).