def Hex.Conway.luebeckConwayPolynomial_179_3 : FpPoly 179

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_179_3_monic : DensePoly.Monic luebeckConwayPolynomial_179_3

Monicity of C(179, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_179_3_degree_pos : 0 < luebeckConwayPolynomial_179_3.degree

Positive degree of C(179, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_179_3 : luebeckConwayPolynomial? 179 3 = some luebeckConwayPolynomial_179_3

Lookup identifies the imported C(179, 3).

def Hex.Conway.luebeckConwayPolynomial_223_3 : FpPoly 223

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_223_3_monic : DensePoly.Monic luebeckConwayPolynomial_223_3

Monicity of C(223, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_223_3_degree_pos : 0 < luebeckConwayPolynomial_223_3.degree

Positive degree of C(223, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_223_3 : luebeckConwayPolynomial? 223 3 = some luebeckConwayPolynomial_223_3

Lookup identifies the imported C(223, 3).

def Hex.Conway.luebeckConwayPolynomial_251_3 : FpPoly 251

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_251_3_monic : DensePoly.Monic luebeckConwayPolynomial_251_3

Monicity of C(251, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_251_3_degree_pos : 0 < luebeckConwayPolynomial_251_3.degree

Positive degree of C(251, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_251_3 : luebeckConwayPolynomial? 251 3 = some luebeckConwayPolynomial_251_3

Lookup identifies the imported C(251, 3).

def Hex.Conway.luebeckConwayPolynomial_839_3 : FpPoly 839

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_839_3_monic : DensePoly.Monic luebeckConwayPolynomial_839_3

Monicity of C(839, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_839_3_degree_pos : 0 < luebeckConwayPolynomial_839_3.degree

Positive degree of C(839, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_839_3 : luebeckConwayPolynomial? 839 3 = some luebeckConwayPolynomial_839_3

Lookup identifies the imported C(839, 3).

def Hex.Conway.luebeckConwayPolynomial_103_3 : FpPoly 103

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_103_3_monic : DensePoly.Monic luebeckConwayPolynomial_103_3

Monicity of C(103, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_103_3_degree_pos : 0 < luebeckConwayPolynomial_103_3.degree

Positive degree of C(103, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_103_3 : luebeckConwayPolynomial? 103 3 = some luebeckConwayPolynomial_103_3

Lookup identifies the imported C(103, 3).

def Hex.Conway.luebeckConwayPolynomial_257_3 : FpPoly 257

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_257_3_monic : DensePoly.Monic luebeckConwayPolynomial_257_3

Monicity of C(257, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_257_3_degree_pos : 0 < luebeckConwayPolynomial_257_3.degree

Positive degree of C(257, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_257_3 : luebeckConwayPolynomial? 257 3 = some luebeckConwayPolynomial_257_3

Lookup identifies the imported C(257, 3).

def Hex.Conway.luebeckConwayPolynomial_2_7 : FpPoly 2

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_2_7_monic : DensePoly.Monic luebeckConwayPolynomial_2_7

Monicity of C(2, 7).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_2_7_degree_pos : 0 < luebeckConwayPolynomial_2_7.degree

Positive degree of C(2, 7).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_2_7 : luebeckConwayPolynomial? 2 7 = some luebeckConwayPolynomial_2_7

Lookup identifies the imported C(2, 7).

def Hex.Conway.luebeckConwayPolynomial_47_3 : FpPoly 47

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_47_3_monic : DensePoly.Monic luebeckConwayPolynomial_47_3

Monicity of C(47, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_47_3_degree_pos : 0 < luebeckConwayPolynomial_47_3.degree

Positive degree of C(47, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_47_3 : luebeckConwayPolynomial? 47 3 = some luebeckConwayPolynomial_47_3

Lookup identifies the imported C(47, 3).

def Hex.Conway.luebeckConwayPolynomial_5_4 : FpPoly 5

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_5_4_monic : DensePoly.Monic luebeckConwayPolynomial_5_4

Monicity of C(5, 4).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_5_4_degree_pos : 0 < luebeckConwayPolynomial_5_4.degree

Positive degree of C(5, 4).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_5_4 : luebeckConwayPolynomial? 5 4 = some luebeckConwayPolynomial_5_4

Lookup identifies the imported C(5, 4).

def Hex.Conway.luebeckConwayPolynomial_89_3 : FpPoly 89

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_89_3_monic : DensePoly.Monic luebeckConwayPolynomial_89_3

Monicity of C(89, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_89_3_degree_pos : 0 < luebeckConwayPolynomial_89_3.degree

Positive degree of C(89, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_89_3 : luebeckConwayPolynomial? 89 3 = some luebeckConwayPolynomial_89_3

Lookup identifies the imported C(89, 3).

def Hex.Conway.luebeckConwayPolynomial_29_3 : FpPoly 29

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_29_3_monic : DensePoly.Monic luebeckConwayPolynomial_29_3

Monicity of C(29, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_29_3_degree_pos : 0 < luebeckConwayPolynomial_29_3.degree

Positive degree of C(29, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_29_3 : luebeckConwayPolynomial? 29 3 = some luebeckConwayPolynomial_29_3

Lookup identifies the imported C(29, 3).

def Hex.Conway.luebeckConwayPolynomial_659_2 : FpPoly 659

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_659_2_monic : DensePoly.Monic luebeckConwayPolynomial_659_2

Monicity of C(659, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_659_2_degree_pos : 0 < luebeckConwayPolynomial_659_2.degree

Positive degree of C(659, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_659_2 : luebeckConwayPolynomial? 659 2 = some luebeckConwayPolynomial_659_2

Lookup identifies the imported C(659, 2).

def Hex.Conway.luebeckConwayPolynomial_419_2 : FpPoly 419

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_419_2_monic : DensePoly.Monic luebeckConwayPolynomial_419_2

Monicity of C(419, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_419_2_degree_pos : 0 < luebeckConwayPolynomial_419_2.degree

Positive degree of C(419, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_419_2 : luebeckConwayPolynomial? 419 2 = some luebeckConwayPolynomial_419_2

Lookup identifies the imported C(419, 2).

def Hex.Conway.luebeckConwayPolynomial_521_2 : FpPoly 521

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_521_2_monic : DensePoly.Monic luebeckConwayPolynomial_521_2

Monicity of C(521, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_521_2_degree_pos : 0 < luebeckConwayPolynomial_521_2.degree

Positive degree of C(521, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_521_2 : luebeckConwayPolynomial? 521 2 = some luebeckConwayPolynomial_521_2

Lookup identifies the imported C(521, 2).

def Hex.Conway.luebeckConwayPolynomial_601_2 : FpPoly 601

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_601_2_monic : DensePoly.Monic luebeckConwayPolynomial_601_2

Monicity of C(601, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_601_2_degree_pos : 0 < luebeckConwayPolynomial_601_2.degree

Positive degree of C(601, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_601_2 : luebeckConwayPolynomial? 601 2 = some luebeckConwayPolynomial_601_2

Lookup identifies the imported C(601, 2).

def Hex.Conway.luebeckConwayPolynomial_643_2 : FpPoly 643

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_643_2_monic : DensePoly.Monic luebeckConwayPolynomial_643_2

Monicity of C(643, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_643_2_degree_pos : 0 < luebeckConwayPolynomial_643_2.degree

Positive degree of C(643, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_643_2 : luebeckConwayPolynomial? 643 2 = some luebeckConwayPolynomial_643_2

Lookup identifies the imported C(643, 2).

def Hex.Conway.luebeckConwayPolynomial_701_2 : FpPoly 701

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_701_2_monic : DensePoly.Monic luebeckConwayPolynomial_701_2

Monicity of C(701, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_701_2_degree_pos : 0 < luebeckConwayPolynomial_701_2.degree

Positive degree of C(701, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_701_2 : luebeckConwayPolynomial? 701 2 = some luebeckConwayPolynomial_701_2

Lookup identifies the imported C(701, 2).

def Hex.Conway.luebeckConwayPolynomial_743_2 : FpPoly 743

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_743_2_monic : DensePoly.Monic luebeckConwayPolynomial_743_2

Monicity of C(743, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_743_2_degree_pos : 0 < luebeckConwayPolynomial_743_2.degree

Positive degree of C(743, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_743_2 : luebeckConwayPolynomial? 743 2 = some luebeckConwayPolynomial_743_2

Lookup identifies the imported C(743, 2).

def Hex.Conway.luebeckConwayPolynomial_811_2 : FpPoly 811

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_811_2_monic : DensePoly.Monic luebeckConwayPolynomial_811_2

Monicity of C(811, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_811_2_degree_pos : 0 < luebeckConwayPolynomial_811_2.degree

Positive degree of C(811, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_811_2 : luebeckConwayPolynomial? 811 2 = some luebeckConwayPolynomial_811_2

Lookup identifies the imported C(811, 2).

def Hex.Conway.luebeckConwayPolynomial_839_2 : FpPoly 839

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_839_2_monic : DensePoly.Monic luebeckConwayPolynomial_839_2

Monicity of C(839, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_839_2_degree_pos : 0 < luebeckConwayPolynomial_839_2.degree

Positive degree of C(839, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_839_2 : luebeckConwayPolynomial? 839 2 = some luebeckConwayPolynomial_839_2

Lookup identifies the imported C(839, 2).

def Hex.Conway.luebeckConwayPolynomial_883_2 : FpPoly 883

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_883_2_monic : DensePoly.Monic luebeckConwayPolynomial_883_2

Monicity of C(883, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_883_2_degree_pos : 0 < luebeckConwayPolynomial_883_2.degree

Positive degree of C(883, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_883_2 : luebeckConwayPolynomial? 883 2 = some luebeckConwayPolynomial_883_2

Lookup identifies the imported C(883, 2).

def Hex.Conway.luebeckConwayPolynomial_941_2 : FpPoly 941

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_941_2_monic : DensePoly.Monic luebeckConwayPolynomial_941_2

Monicity of C(941, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_941_2_degree_pos : 0 < luebeckConwayPolynomial_941_2.degree

Positive degree of C(941, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_941_2 : luebeckConwayPolynomial? 941 2 = some luebeckConwayPolynomial_941_2

Lookup identifies the imported C(941, 2).

def Hex.Conway.luebeckConwayPolynomial_991_2 : FpPoly 991

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_991_2_monic : DensePoly.Monic luebeckConwayPolynomial_991_2

Monicity of C(991, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_991_2_degree_pos : 0 < luebeckConwayPolynomial_991_2.degree

Positive degree of C(991, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_991_2 : luebeckConwayPolynomial? 991 2 = some luebeckConwayPolynomial_991_2

Lookup identifies the imported C(991, 2).

def Hex.Conway.luebeckConwayPolynomial_373_2 : FpPoly 373

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_373_2_monic : DensePoly.Monic luebeckConwayPolynomial_373_2

Monicity of C(373, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_373_2_degree_pos : 0 < luebeckConwayPolynomial_373_2.degree

Positive degree of C(373, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_373_2 : luebeckConwayPolynomial? 373 2 = some luebeckConwayPolynomial_373_2

Lookup identifies the imported C(373, 2).