def Hex.Conway.luebeckConwayPolynomial_277_1 : FpPoly 277

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_277_1_monic : DensePoly.Monic luebeckConwayPolynomial_277_1

Monicity of C(277, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_277_1_degree_pos : 0 < luebeckConwayPolynomial_277_1.degree

Positive degree of C(277, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_277_1 : luebeckConwayPolynomial? 277 1 = some luebeckConwayPolynomial_277_1

Lookup identifies the imported C(277, 1).

def Hex.Conway.luebeckConwayPolynomial_311_1 : FpPoly 311

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_311_1_monic : DensePoly.Monic luebeckConwayPolynomial_311_1

Monicity of C(311, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_311_1_degree_pos : 0 < luebeckConwayPolynomial_311_1.degree

Positive degree of C(311, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_311_1 : luebeckConwayPolynomial? 311 1 = some luebeckConwayPolynomial_311_1

Lookup identifies the imported C(311, 1).

def Hex.Conway.luebeckConwayPolynomial_367_1 : FpPoly 367

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_367_1_monic : DensePoly.Monic luebeckConwayPolynomial_367_1

Monicity of C(367, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_367_1_degree_pos : 0 < luebeckConwayPolynomial_367_1.degree

Positive degree of C(367, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_367_1 : luebeckConwayPolynomial? 367 1 = some luebeckConwayPolynomial_367_1

Lookup identifies the imported C(367, 1).

def Hex.Conway.luebeckConwayPolynomial_409_1 : FpPoly 409

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_409_1_monic : DensePoly.Monic luebeckConwayPolynomial_409_1

Monicity of C(409, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_409_1_degree_pos : 0 < luebeckConwayPolynomial_409_1.degree

Positive degree of C(409, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_409_1 : luebeckConwayPolynomial? 409 1 = some luebeckConwayPolynomial_409_1

Lookup identifies the imported C(409, 1).

def Hex.Conway.luebeckConwayPolynomial_443_1 : FpPoly 443

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_443_1_monic : DensePoly.Monic luebeckConwayPolynomial_443_1

Monicity of C(443, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_443_1_degree_pos : 0 < luebeckConwayPolynomial_443_1.degree

Positive degree of C(443, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_443_1 : luebeckConwayPolynomial? 443 1 = some luebeckConwayPolynomial_443_1

Lookup identifies the imported C(443, 1).

def Hex.Conway.luebeckConwayPolynomial_499_1 : FpPoly 499

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_499_1_monic : DensePoly.Monic luebeckConwayPolynomial_499_1

Monicity of C(499, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_499_1_degree_pos : 0 < luebeckConwayPolynomial_499_1.degree

Positive degree of C(499, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_499_1 : luebeckConwayPolynomial? 499 1 = some luebeckConwayPolynomial_499_1

Lookup identifies the imported C(499, 1).

def Hex.Conway.luebeckConwayPolynomial_191_1 : FpPoly 191

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_191_1_monic : DensePoly.Monic luebeckConwayPolynomial_191_1

Monicity of C(191, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_191_1_degree_pos : 0 < luebeckConwayPolynomial_191_1.degree

Positive degree of C(191, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_191_1 : luebeckConwayPolynomial? 191 1 = some luebeckConwayPolynomial_191_1

Lookup identifies the imported C(191, 1).

def Hex.Conway.luebeckConwayPolynomial_239_1 : FpPoly 239

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_239_1_monic : DensePoly.Monic luebeckConwayPolynomial_239_1

Monicity of C(239, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_239_1_degree_pos : 0 < luebeckConwayPolynomial_239_1.degree

Positive degree of C(239, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_239_1 : luebeckConwayPolynomial? 239 1 = some luebeckConwayPolynomial_239_1

Lookup identifies the imported C(239, 1).

def Hex.Conway.luebeckConwayPolynomial_79_1 : FpPoly 79

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_79_1_monic : DensePoly.Monic luebeckConwayPolynomial_79_1

Monicity of C(79, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_79_1_degree_pos : 0 < luebeckConwayPolynomial_79_1.degree

Positive degree of C(79, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_79_1 : luebeckConwayPolynomial? 79 1 = some luebeckConwayPolynomial_79_1

Lookup identifies the imported C(79, 1).

def Hex.Conway.luebeckConwayPolynomial_563_1 : FpPoly 563

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_563_1_monic : DensePoly.Monic luebeckConwayPolynomial_563_1

Monicity of C(563, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_563_1_degree_pos : 0 < luebeckConwayPolynomial_563_1.degree

Positive degree of C(563, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_563_1 : luebeckConwayPolynomial? 563 1 = some luebeckConwayPolynomial_563_1

Lookup identifies the imported C(563, 1).

def Hex.Conway.luebeckConwayPolynomial_593_1 : FpPoly 593

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_593_1_monic : DensePoly.Monic luebeckConwayPolynomial_593_1

Monicity of C(593, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_593_1_degree_pos : 0 < luebeckConwayPolynomial_593_1.degree

Positive degree of C(593, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_593_1 : luebeckConwayPolynomial? 593 1 = some luebeckConwayPolynomial_593_1

Lookup identifies the imported C(593, 1).

def Hex.Conway.luebeckConwayPolynomial_719_1 : FpPoly 719

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_719_1_monic : DensePoly.Monic luebeckConwayPolynomial_719_1

Monicity of C(719, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_719_1_degree_pos : 0 < luebeckConwayPolynomial_719_1.degree

Positive degree of C(719, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_719_1 : luebeckConwayPolynomial? 719 1 = some luebeckConwayPolynomial_719_1

Lookup identifies the imported C(719, 1).

def Hex.Conway.luebeckConwayPolynomial_809_1 : FpPoly 809

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_809_1_monic : DensePoly.Monic luebeckConwayPolynomial_809_1

Monicity of C(809, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_809_1_degree_pos : 0 < luebeckConwayPolynomial_809_1.degree

Positive degree of C(809, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_809_1 : luebeckConwayPolynomial? 809 1 = some luebeckConwayPolynomial_809_1

Lookup identifies the imported C(809, 1).

def Hex.Conway.luebeckConwayPolynomial_887_1 : FpPoly 887

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_887_1_monic : DensePoly.Monic luebeckConwayPolynomial_887_1

Monicity of C(887, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_887_1_degree_pos : 0 < luebeckConwayPolynomial_887_1.degree

Positive degree of C(887, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_887_1 : luebeckConwayPolynomial? 887 1 = some luebeckConwayPolynomial_887_1

Lookup identifies the imported C(887, 1).

def Hex.Conway.luebeckConwayPolynomial_43_1 : FpPoly 43

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_43_1_monic : DensePoly.Monic luebeckConwayPolynomial_43_1

Monicity of C(43, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_43_1_degree_pos : 0 < luebeckConwayPolynomial_43_1.degree

Positive degree of C(43, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_43_1 : luebeckConwayPolynomial? 43 1 = some luebeckConwayPolynomial_43_1

Lookup identifies the imported C(43, 1).

def Hex.Conway.luebeckConwayPolynomial_263_1 : FpPoly 263

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_263_1_monic : DensePoly.Monic luebeckConwayPolynomial_263_1

Monicity of C(263, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_263_1_degree_pos : 0 < luebeckConwayPolynomial_263_1.degree

Positive degree of C(263, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_263_1 : luebeckConwayPolynomial? 263 1 = some luebeckConwayPolynomial_263_1

Lookup identifies the imported C(263, 1).

def Hex.Conway.luebeckConwayPolynomial_347_1 : FpPoly 347

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_347_1_monic : DensePoly.Monic luebeckConwayPolynomial_347_1

Monicity of C(347, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_347_1_degree_pos : 0 < luebeckConwayPolynomial_347_1.degree

Positive degree of C(347, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_347_1 : luebeckConwayPolynomial? 347 1 = some luebeckConwayPolynomial_347_1

Lookup identifies the imported C(347, 1).

def Hex.Conway.luebeckConwayPolynomial_389_1 : FpPoly 389

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_389_1_monic : DensePoly.Monic luebeckConwayPolynomial_389_1

Monicity of C(389, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_389_1_degree_pos : 0 < luebeckConwayPolynomial_389_1.degree

Positive degree of C(389, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_389_1 : luebeckConwayPolynomial? 389 1 = some luebeckConwayPolynomial_389_1

Lookup identifies the imported C(389, 1).

def Hex.Conway.luebeckConwayPolynomial_467_1 : FpPoly 467

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_467_1_monic : DensePoly.Monic luebeckConwayPolynomial_467_1

Monicity of C(467, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_467_1_degree_pos : 0 < luebeckConwayPolynomial_467_1.degree

Positive degree of C(467, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_467_1 : luebeckConwayPolynomial? 467 1 = some luebeckConwayPolynomial_467_1

Lookup identifies the imported C(467, 1).

def Hex.Conway.luebeckConwayPolynomial_509_1 : FpPoly 509

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_509_1_monic : DensePoly.Monic luebeckConwayPolynomial_509_1

Monicity of C(509, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_509_1_degree_pos : 0 < luebeckConwayPolynomial_509_1.degree

Positive degree of C(509, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_509_1 : luebeckConwayPolynomial? 509 1 = some luebeckConwayPolynomial_509_1

Lookup identifies the imported C(509, 1).

def Hex.Conway.luebeckConwayPolynomial_167_1 : FpPoly 167

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_167_1_monic : DensePoly.Monic luebeckConwayPolynomial_167_1

Monicity of C(167, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_167_1_degree_pos : 0 < luebeckConwayPolynomial_167_1.degree

Positive degree of C(167, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_167_1 : luebeckConwayPolynomial? 167 1 = some luebeckConwayPolynomial_167_1

Lookup identifies the imported C(167, 1).

def Hex.Conway.luebeckConwayPolynomial_197_1 : FpPoly 197

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_197_1_monic : DensePoly.Monic luebeckConwayPolynomial_197_1

Monicity of C(197, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_197_1_degree_pos : 0 < luebeckConwayPolynomial_197_1.degree

Positive degree of C(197, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_197_1 : luebeckConwayPolynomial? 197 1 = some luebeckConwayPolynomial_197_1

Lookup identifies the imported C(197, 1).

def Hex.Conway.luebeckConwayPolynomial_31_1 : FpPoly 31

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_31_1_monic : DensePoly.Monic luebeckConwayPolynomial_31_1

Monicity of C(31, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_31_1_degree_pos : 0 < luebeckConwayPolynomial_31_1.degree

Positive degree of C(31, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_31_1 : luebeckConwayPolynomial? 31 1 = some luebeckConwayPolynomial_31_1

Lookup identifies the imported C(31, 1).

def Hex.Conway.luebeckConwayPolynomial_101_1 : FpPoly 101

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_101_1_monic : DensePoly.Monic luebeckConwayPolynomial_101_1

Monicity of C(101, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_101_1_degree_pos : 0 < luebeckConwayPolynomial_101_1.degree

Positive degree of C(101, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_101_1 : luebeckConwayPolynomial? 101 1 = some luebeckConwayPolynomial_101_1

Lookup identifies the imported C(101, 1).