def Hex.Conway.luebeckConwayPolynomial_431_1 : FpPoly 431

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_431_1_monic : DensePoly.Monic luebeckConwayPolynomial_431_1

Monicity of C(431, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_431_1_degree_pos : 0 < luebeckConwayPolynomial_431_1.degree

Positive degree of C(431, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_431_1 : luebeckConwayPolynomial? 431 1 = some luebeckConwayPolynomial_431_1

Lookup identifies the imported C(431, 1).

def Hex.Conway.luebeckConwayPolynomial_461_1 : FpPoly 461

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_461_1_monic : DensePoly.Monic luebeckConwayPolynomial_461_1

Monicity of C(461, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_461_1_degree_pos : 0 < luebeckConwayPolynomial_461_1.degree

Positive degree of C(461, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_461_1 : luebeckConwayPolynomial? 461 1 = some luebeckConwayPolynomial_461_1

Lookup identifies the imported C(461, 1).

def Hex.Conway.luebeckConwayPolynomial_139_1 : FpPoly 139

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_139_1_monic : DensePoly.Monic luebeckConwayPolynomial_139_1

Monicity of C(139, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_139_1_degree_pos : 0 < luebeckConwayPolynomial_139_1.degree

Positive degree of C(139, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_139_1 : luebeckConwayPolynomial? 139 1 = some luebeckConwayPolynomial_139_1

Lookup identifies the imported C(139, 1).

def Hex.Conway.luebeckConwayPolynomial_181_1 : FpPoly 181

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_181_1_monic : DensePoly.Monic luebeckConwayPolynomial_181_1

Monicity of C(181, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_181_1_degree_pos : 0 < luebeckConwayPolynomial_181_1.degree

Positive degree of C(181, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_181_1 : luebeckConwayPolynomial? 181 1 = some luebeckConwayPolynomial_181_1

Lookup identifies the imported C(181, 1).

def Hex.Conway.luebeckConwayPolynomial_229_1 : FpPoly 229

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_229_1_monic : DensePoly.Monic luebeckConwayPolynomial_229_1

Monicity of C(229, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_229_1_degree_pos : 0 < luebeckConwayPolynomial_229_1.degree

Positive degree of C(229, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_229_1 : luebeckConwayPolynomial? 229 1 = some luebeckConwayPolynomial_229_1

Lookup identifies the imported C(229, 1).

def Hex.Conway.luebeckConwayPolynomial_71_1 : FpPoly 71

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_71_1_monic : DensePoly.Monic luebeckConwayPolynomial_71_1

Monicity of C(71, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_71_1_degree_pos : 0 < luebeckConwayPolynomial_71_1.degree

Positive degree of C(71, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_71_1 : luebeckConwayPolynomial? 71 1 = some luebeckConwayPolynomial_71_1

Lookup identifies the imported C(71, 1).

def Hex.Conway.luebeckConwayPolynomial_557_1 : FpPoly 557

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_557_1_monic : DensePoly.Monic luebeckConwayPolynomial_557_1

Monicity of C(557, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_557_1_degree_pos : 0 < luebeckConwayPolynomial_557_1.degree

Positive degree of C(557, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_557_1 : luebeckConwayPolynomial? 557 1 = some luebeckConwayPolynomial_557_1

Lookup identifies the imported C(557, 1).

def Hex.Conway.luebeckConwayPolynomial_577_1 : FpPoly 577

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_577_1_monic : DensePoly.Monic luebeckConwayPolynomial_577_1

Monicity of C(577, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_577_1_degree_pos : 0 < luebeckConwayPolynomial_577_1.degree

Positive degree of C(577, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_577_1 : luebeckConwayPolynomial? 577 1 = some luebeckConwayPolynomial_577_1

Lookup identifies the imported C(577, 1).

def Hex.Conway.luebeckConwayPolynomial_653_1 : FpPoly 653

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_653_1_monic : DensePoly.Monic luebeckConwayPolynomial_653_1

Monicity of C(653, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_653_1_degree_pos : 0 < luebeckConwayPolynomial_653_1.degree

Positive degree of C(653, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_653_1 : luebeckConwayPolynomial? 653 1 = some luebeckConwayPolynomial_653_1

Lookup identifies the imported C(653, 1).

def Hex.Conway.luebeckConwayPolynomial_773_1 : FpPoly 773

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_773_1_monic : DensePoly.Monic luebeckConwayPolynomial_773_1

Monicity of C(773, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_773_1_degree_pos : 0 < luebeckConwayPolynomial_773_1.degree

Positive degree of C(773, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_773_1 : luebeckConwayPolynomial? 773 1 = some luebeckConwayPolynomial_773_1

Lookup identifies the imported C(773, 1).

def Hex.Conway.luebeckConwayPolynomial_857_1 : FpPoly 857

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_857_1_monic : DensePoly.Monic luebeckConwayPolynomial_857_1

Monicity of C(857, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_857_1_degree_pos : 0 < luebeckConwayPolynomial_857_1.degree

Positive degree of C(857, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_857_1 : luebeckConwayPolynomial? 857 1 = some luebeckConwayPolynomial_857_1

Lookup identifies the imported C(857, 1).

def Hex.Conway.luebeckConwayPolynomial_977_1 : FpPoly 977

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_977_1_monic : DensePoly.Monic luebeckConwayPolynomial_977_1

Monicity of C(977, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_977_1_degree_pos : 0 < luebeckConwayPolynomial_977_1.degree

Positive degree of C(977, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_977_1 : luebeckConwayPolynomial? 977 1 = some luebeckConwayPolynomial_977_1

Lookup identifies the imported C(977, 1).

def Hex.Conway.luebeckConwayPolynomial_269_1 : FpPoly 269

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_269_1_monic : DensePoly.Monic luebeckConwayPolynomial_269_1

Monicity of C(269, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_269_1_degree_pos : 0 < luebeckConwayPolynomial_269_1.degree

Positive degree of C(269, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_269_1 : luebeckConwayPolynomial? 269 1 = some luebeckConwayPolynomial_269_1

Lookup identifies the imported C(269, 1).

def Hex.Conway.luebeckConwayPolynomial_353_1 : FpPoly 353

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_353_1_monic : DensePoly.Monic luebeckConwayPolynomial_353_1

Monicity of C(353, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_353_1_degree_pos : 0 < luebeckConwayPolynomial_353_1.degree

Positive degree of C(353, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_353_1 : luebeckConwayPolynomial? 353 1 = some luebeckConwayPolynomial_353_1

Lookup identifies the imported C(353, 1).

def Hex.Conway.luebeckConwayPolynomial_401_1 : FpPoly 401

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_401_1_monic : DensePoly.Monic luebeckConwayPolynomial_401_1

Monicity of C(401, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_401_1_degree_pos : 0 < luebeckConwayPolynomial_401_1.degree

Positive degree of C(401, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_401_1 : luebeckConwayPolynomial? 401 1 = some luebeckConwayPolynomial_401_1

Lookup identifies the imported C(401, 1).

def Hex.Conway.luebeckConwayPolynomial_479_1 : FpPoly 479

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_479_1_monic : DensePoly.Monic luebeckConwayPolynomial_479_1

Monicity of C(479, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_479_1_degree_pos : 0 < luebeckConwayPolynomial_479_1.degree

Positive degree of C(479, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_479_1 : luebeckConwayPolynomial? 479 1 = some luebeckConwayPolynomial_479_1

Lookup identifies the imported C(479, 1).

def Hex.Conway.luebeckConwayPolynomial_2_2 : FpPoly 2

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_2_2_monic : DensePoly.Monic luebeckConwayPolynomial_2_2

Monicity of C(2, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_2_2_degree_pos : 0 < luebeckConwayPolynomial_2_2.degree

Positive degree of C(2, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_2_2 : luebeckConwayPolynomial? 2 2 = some luebeckConwayPolynomial_2_2

Lookup identifies the imported C(2, 2).

def Hex.Conway.luebeckConwayPolynomial_149_1 : FpPoly 149

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_149_1_monic : DensePoly.Monic luebeckConwayPolynomial_149_1

Monicity of C(149, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_149_1_degree_pos : 0 < luebeckConwayPolynomial_149_1.degree

Positive degree of C(149, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_149_1 : luebeckConwayPolynomial? 149 1 = some luebeckConwayPolynomial_149_1

Lookup identifies the imported C(149, 1).

def Hex.Conway.luebeckConwayPolynomial_179_1 : FpPoly 179

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_179_1_monic : DensePoly.Monic luebeckConwayPolynomial_179_1

Monicity of C(179, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_179_1_degree_pos : 0 < luebeckConwayPolynomial_179_1.degree

Positive degree of C(179, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_179_1 : luebeckConwayPolynomial? 179 1 = some luebeckConwayPolynomial_179_1

Lookup identifies the imported C(179, 1).

def Hex.Conway.luebeckConwayPolynomial_233_1 : FpPoly 233

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_233_1_monic : DensePoly.Monic luebeckConwayPolynomial_233_1

Monicity of C(233, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_233_1_degree_pos : 0 < luebeckConwayPolynomial_233_1.degree

Positive degree of C(233, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_233_1 : luebeckConwayPolynomial? 233 1 = some luebeckConwayPolynomial_233_1

Lookup identifies the imported C(233, 1).

def Hex.Conway.luebeckConwayPolynomial_89_1 : FpPoly 89

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_89_1_monic : DensePoly.Monic luebeckConwayPolynomial_89_1

Monicity of C(89, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_89_1_degree_pos : 0 < luebeckConwayPolynomial_89_1.degree

Positive degree of C(89, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_89_1 : luebeckConwayPolynomial? 89 1 = some luebeckConwayPolynomial_89_1

Lookup identifies the imported C(89, 1).

def Hex.Conway.luebeckConwayPolynomial_109_1 : FpPoly 109

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_109_1_monic : DensePoly.Monic luebeckConwayPolynomial_109_1

Monicity of C(109, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_109_1_degree_pos : 0 < luebeckConwayPolynomial_109_1.degree

Positive degree of C(109, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_109_1 : luebeckConwayPolynomial? 109 1 = some luebeckConwayPolynomial_109_1

Lookup identifies the imported C(109, 1).

def Hex.Conway.luebeckConwayPolynomial_53_1 : FpPoly 53

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_53_1_monic : DensePoly.Monic luebeckConwayPolynomial_53_1

Monicity of C(53, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_53_1_degree_pos : 0 < luebeckConwayPolynomial_53_1.degree

Positive degree of C(53, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_53_1 : luebeckConwayPolynomial? 53 1 = some luebeckConwayPolynomial_53_1

Lookup identifies the imported C(53, 1).

def Hex.Conway.luebeckConwayPolynomial_29_1 : FpPoly 29

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_29_1_monic : DensePoly.Monic luebeckConwayPolynomial_29_1

Monicity of C(29, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_29_1_degree_pos : 0 < luebeckConwayPolynomial_29_1.degree

Positive degree of C(29, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_29_1 : luebeckConwayPolynomial? 29 1 = some luebeckConwayPolynomial_29_1

Lookup identifies the imported C(29, 1).