def Hex.Conway.luebeckConwayPolynomial_223_2 : FpPoly 223

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_223_2_monic : DensePoly.Monic luebeckConwayPolynomial_223_2

Monicity of C(223, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_223_2_degree_pos : 0 < luebeckConwayPolynomial_223_2.degree

Positive degree of C(223, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_223_2 : luebeckConwayPolynomial? 223 2 = some luebeckConwayPolynomial_223_2

Lookup identifies the imported C(223, 2).

def Hex.Conway.luebeckConwayPolynomial_251_2 : FpPoly 251

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_251_2_monic : DensePoly.Monic luebeckConwayPolynomial_251_2

Monicity of C(251, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_251_2_degree_pos : 0 < luebeckConwayPolynomial_251_2.degree

Positive degree of C(251, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_251_2 : luebeckConwayPolynomial? 251 2 = some luebeckConwayPolynomial_251_2

Lookup identifies the imported C(251, 2).

def Hex.Conway.luebeckConwayPolynomial_71_2 : FpPoly 71

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_71_2_monic : DensePoly.Monic luebeckConwayPolynomial_71_2

Monicity of C(71, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_71_2_degree_pos : 0 < luebeckConwayPolynomial_71_2.degree

Positive degree of C(71, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_71_2 : luebeckConwayPolynomial? 71 2 = some luebeckConwayPolynomial_71_2

Lookup identifies the imported C(71, 2).

def Hex.Conway.luebeckConwayPolynomial_89_2 : FpPoly 89

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_89_2_monic : DensePoly.Monic luebeckConwayPolynomial_89_2

Monicity of C(89, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_89_2_degree_pos : 0 < luebeckConwayPolynomial_89_2.degree

Positive degree of C(89, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_89_2 : luebeckConwayPolynomial? 89 2 = some luebeckConwayPolynomial_89_2

Lookup identifies the imported C(89, 2).

def Hex.Conway.luebeckConwayPolynomial_113_2 : FpPoly 113

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_113_2_monic : DensePoly.Monic luebeckConwayPolynomial_113_2

Monicity of C(113, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_113_2_degree_pos : 0 < luebeckConwayPolynomial_113_2.degree

Positive degree of C(113, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_113_2 : luebeckConwayPolynomial? 113 2 = some luebeckConwayPolynomial_113_2

Lookup identifies the imported C(113, 2).

def Hex.Conway.luebeckConwayPolynomial_43_2 : FpPoly 43

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_43_2_monic : DensePoly.Monic luebeckConwayPolynomial_43_2

Monicity of C(43, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_43_2_degree_pos : 0 < luebeckConwayPolynomial_43_2.degree

Positive degree of C(43, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_43_2 : luebeckConwayPolynomial? 43 2 = some luebeckConwayPolynomial_43_2

Lookup identifies the imported C(43, 2).

def Hex.Conway.luebeckConwayPolynomial_163_2 : FpPoly 163

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_163_2_monic : DensePoly.Monic luebeckConwayPolynomial_163_2

Monicity of C(163, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_163_2_degree_pos : 0 < luebeckConwayPolynomial_163_2.degree

Positive degree of C(163, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_163_2 : luebeckConwayPolynomial? 163 2 = some luebeckConwayPolynomial_163_2

Lookup identifies the imported C(163, 2).

def Hex.Conway.luebeckConwayPolynomial_127_2 : FpPoly 127

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_127_2_monic : DensePoly.Monic luebeckConwayPolynomial_127_2

Monicity of C(127, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_127_2_degree_pos : 0 < luebeckConwayPolynomial_127_2.degree

Positive degree of C(127, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_127_2 : luebeckConwayPolynomial? 127 2 = some luebeckConwayPolynomial_127_2

Lookup identifies the imported C(127, 2).

def Hex.Conway.luebeckConwayPolynomial_53_2 : FpPoly 53

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_53_2_monic : DensePoly.Monic luebeckConwayPolynomial_53_2

Monicity of C(53, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_53_2_degree_pos : 0 < luebeckConwayPolynomial_53_2.degree

Positive degree of C(53, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_53_2 : luebeckConwayPolynomial? 53 2 = some luebeckConwayPolynomial_53_2

Lookup identifies the imported C(53, 2).

def Hex.Conway.luebeckConwayPolynomial_31_2 : FpPoly 31

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_31_2_monic : DensePoly.Monic luebeckConwayPolynomial_31_2

Monicity of C(31, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_31_2_degree_pos : 0 < luebeckConwayPolynomial_31_2.degree

Positive degree of C(31, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_31_2 : luebeckConwayPolynomial? 31 2 = some luebeckConwayPolynomial_31_2

Lookup identifies the imported C(31, 2).

def Hex.Conway.luebeckConwayPolynomial_2_3 : FpPoly 2

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_2_3_monic : DensePoly.Monic luebeckConwayPolynomial_2_3

Monicity of C(2, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_2_3_degree_pos : 0 < luebeckConwayPolynomial_2_3.degree

Positive degree of C(2, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_2_3 : luebeckConwayPolynomial? 2 3 = some luebeckConwayPolynomial_2_3

Lookup identifies the imported C(2, 3).

def Hex.Conway.luebeckConwayPolynomial_5_2 : FpPoly 5

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_5_2_monic : DensePoly.Monic luebeckConwayPolynomial_5_2

Monicity of C(5, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_5_2_degree_pos : 0 < luebeckConwayPolynomial_5_2.degree

Positive degree of C(5, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_5_2 : luebeckConwayPolynomial? 5 2 = some luebeckConwayPolynomial_5_2

Lookup identifies the imported C(5, 2).

def Hex.Conway.luebeckConwayPolynomial_631_1 : FpPoly 631

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_631_1_monic : DensePoly.Monic luebeckConwayPolynomial_631_1

Monicity of C(631, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_631_1_degree_pos : 0 < luebeckConwayPolynomial_631_1.degree

Positive degree of C(631, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_631_1 : luebeckConwayPolynomial? 631 1 = some luebeckConwayPolynomial_631_1

Lookup identifies the imported C(631, 1).

def Hex.Conway.luebeckConwayPolynomial_911_1 : FpPoly 911

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_911_1_monic : DensePoly.Monic luebeckConwayPolynomial_911_1

Monicity of C(911, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_911_1_degree_pos : 0 < luebeckConwayPolynomial_911_1.degree

Positive degree of C(911, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_911_1 : luebeckConwayPolynomial? 911 1 = some luebeckConwayPolynomial_911_1

Lookup identifies the imported C(911, 1).

def Hex.Conway.luebeckConwayPolynomial_421_1 : FpPoly 421

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_421_1_monic : DensePoly.Monic luebeckConwayPolynomial_421_1

Monicity of C(421, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_421_1_degree_pos : 0 < luebeckConwayPolynomial_421_1.degree

Positive degree of C(421, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_421_1 : luebeckConwayPolynomial? 421 1 = some luebeckConwayPolynomial_421_1

Lookup identifies the imported C(421, 1).

def Hex.Conway.luebeckConwayPolynomial_523_1 : FpPoly 523

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_523_1_monic : DensePoly.Monic luebeckConwayPolynomial_523_1

Monicity of C(523, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_523_1_degree_pos : 0 < luebeckConwayPolynomial_523_1.degree

Positive degree of C(523, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_523_1 : luebeckConwayPolynomial? 523 1 = some luebeckConwayPolynomial_523_1

Lookup identifies the imported C(523, 1).

def Hex.Conway.luebeckConwayPolynomial_607_1 : FpPoly 607

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_607_1_monic : DensePoly.Monic luebeckConwayPolynomial_607_1

Monicity of C(607, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_607_1_degree_pos : 0 < luebeckConwayPolynomial_607_1.degree

Positive degree of C(607, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_607_1 : luebeckConwayPolynomial? 607 1 = some luebeckConwayPolynomial_607_1

Lookup identifies the imported C(607, 1).

def Hex.Conway.luebeckConwayPolynomial_643_1 : FpPoly 643

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_643_1_monic : DensePoly.Monic luebeckConwayPolynomial_643_1

Monicity of C(643, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_643_1_degree_pos : 0 < luebeckConwayPolynomial_643_1.degree

Positive degree of C(643, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_643_1 : luebeckConwayPolynomial? 643 1 = some luebeckConwayPolynomial_643_1

Lookup identifies the imported C(643, 1).

def Hex.Conway.luebeckConwayPolynomial_683_1 : FpPoly 683

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_683_1_monic : DensePoly.Monic luebeckConwayPolynomial_683_1

Monicity of C(683, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_683_1_degree_pos : 0 < luebeckConwayPolynomial_683_1.degree

Positive degree of C(683, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_683_1 : luebeckConwayPolynomial? 683 1 = some luebeckConwayPolynomial_683_1

Lookup identifies the imported C(683, 1).

def Hex.Conway.luebeckConwayPolynomial_733_1 : FpPoly 733

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_733_1_monic : DensePoly.Monic luebeckConwayPolynomial_733_1

Monicity of C(733, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_733_1_degree_pos : 0 < luebeckConwayPolynomial_733_1.degree

Positive degree of C(733, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_733_1 : luebeckConwayPolynomial? 733 1 = some luebeckConwayPolynomial_733_1

Lookup identifies the imported C(733, 1).

def Hex.Conway.luebeckConwayPolynomial_757_1 : FpPoly 757

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_757_1_monic : DensePoly.Monic luebeckConwayPolynomial_757_1

Monicity of C(757, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_757_1_degree_pos : 0 < luebeckConwayPolynomial_757_1.degree

Positive degree of C(757, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_757_1 : luebeckConwayPolynomial? 757 1 = some luebeckConwayPolynomial_757_1

Lookup identifies the imported C(757, 1).

def Hex.Conway.luebeckConwayPolynomial_821_1 : FpPoly 821

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_821_1_monic : DensePoly.Monic luebeckConwayPolynomial_821_1

Monicity of C(821, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_821_1_degree_pos : 0 < luebeckConwayPolynomial_821_1.degree

Positive degree of C(821, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_821_1 : luebeckConwayPolynomial? 821 1 = some luebeckConwayPolynomial_821_1

Lookup identifies the imported C(821, 1).

def Hex.Conway.luebeckConwayPolynomial_853_1 : FpPoly 853

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_853_1_monic : DensePoly.Monic luebeckConwayPolynomial_853_1

Monicity of C(853, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_853_1_degree_pos : 0 < luebeckConwayPolynomial_853_1.degree

Positive degree of C(853, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_853_1 : luebeckConwayPolynomial? 853 1 = some luebeckConwayPolynomial_853_1

Lookup identifies the imported C(853, 1).

def Hex.Conway.luebeckConwayPolynomial_907_1 : FpPoly 907

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_907_1_monic : DensePoly.Monic luebeckConwayPolynomial_907_1

Monicity of C(907, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_907_1_degree_pos : 0 < luebeckConwayPolynomial_907_1.degree

Positive degree of C(907, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_907_1 : luebeckConwayPolynomial? 907 1 = some luebeckConwayPolynomial_907_1

Lookup identifies the imported C(907, 1).