def Hex.Conway.luebeckConwayPolynomial_409_3 : FpPoly 409

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_409_3_monic : DensePoly.Monic luebeckConwayPolynomial_409_3

Monicity of C(409, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_409_3_degree_pos : 0 < luebeckConwayPolynomial_409_3.degree

Positive degree of C(409, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_409_3 : luebeckConwayPolynomial? 409 3 = some luebeckConwayPolynomial_409_3

Lookup identifies the imported C(409, 3).

def Hex.Conway.luebeckConwayPolynomial_479_3 : FpPoly 479

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_479_3_monic : DensePoly.Monic luebeckConwayPolynomial_479_3

Monicity of C(479, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_479_3_degree_pos : 0 < luebeckConwayPolynomial_479_3.degree

Positive degree of C(479, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_479_3 : luebeckConwayPolynomial? 479 3 = some luebeckConwayPolynomial_479_3

Lookup identifies the imported C(479, 3).

def Hex.Conway.luebeckConwayPolynomial_67_3 : FpPoly 67

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_67_3_monic : DensePoly.Monic luebeckConwayPolynomial_67_3

Monicity of C(67, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_67_3_degree_pos : 0 < luebeckConwayPolynomial_67_3.degree

Positive degree of C(67, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_67_3 : luebeckConwayPolynomial? 67 3 = some luebeckConwayPolynomial_67_3

Lookup identifies the imported C(67, 3).

def Hex.Conway.luebeckConwayPolynomial_131_3 : FpPoly 131

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_131_3_monic : DensePoly.Monic luebeckConwayPolynomial_131_3

Monicity of C(131, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_131_3_degree_pos : 0 < luebeckConwayPolynomial_131_3.degree

Positive degree of C(131, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_131_3 : luebeckConwayPolynomial? 131 3 = some luebeckConwayPolynomial_131_3

Lookup identifies the imported C(131, 3).

def Hex.Conway.luebeckConwayPolynomial_197_3 : FpPoly 197

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_197_3_monic : DensePoly.Monic luebeckConwayPolynomial_197_3

Monicity of C(197, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_197_3_degree_pos : 0 < luebeckConwayPolynomial_197_3.degree

Positive degree of C(197, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_197_3 : luebeckConwayPolynomial? 197 3 = some luebeckConwayPolynomial_197_3

Lookup identifies the imported C(197, 3).

def Hex.Conway.luebeckConwayPolynomial_233_3 : FpPoly 233

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_233_3_monic : DensePoly.Monic luebeckConwayPolynomial_233_3

Monicity of C(233, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_233_3_degree_pos : 0 < luebeckConwayPolynomial_233_3.degree

Positive degree of C(233, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_233_3 : luebeckConwayPolynomial? 233 3 = some luebeckConwayPolynomial_233_3

Lookup identifies the imported C(233, 3).

def Hex.Conway.luebeckConwayPolynomial_677_3 : FpPoly 677

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_677_3_monic : DensePoly.Monic luebeckConwayPolynomial_677_3

Monicity of C(677, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_677_3_degree_pos : 0 < luebeckConwayPolynomial_677_3.degree

Positive degree of C(677, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_677_3 : luebeckConwayPolynomial? 677 3 = some luebeckConwayPolynomial_677_3

Lookup identifies the imported C(677, 3).

def Hex.Conway.luebeckConwayPolynomial_71_3 : FpPoly 71

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_71_3_monic : DensePoly.Monic luebeckConwayPolynomial_71_3

Monicity of C(71, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_71_3_degree_pos : 0 < luebeckConwayPolynomial_71_3.degree

Positive degree of C(71, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_71_3 : luebeckConwayPolynomial? 71 3 = some luebeckConwayPolynomial_71_3

Lookup identifies the imported C(71, 3).

def Hex.Conway.luebeckConwayPolynomial_113_3 : FpPoly 113

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_113_3_monic : DensePoly.Monic luebeckConwayPolynomial_113_3

Monicity of C(113, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_113_3_degree_pos : 0 < luebeckConwayPolynomial_113_3.degree

Positive degree of C(113, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_113_3 : luebeckConwayPolynomial? 113 3 = some luebeckConwayPolynomial_113_3

Lookup identifies the imported C(113, 3).

def Hex.Conway.luebeckConwayPolynomial_383_3 : FpPoly 383

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_383_3_monic : DensePoly.Monic luebeckConwayPolynomial_383_3

Monicity of C(383, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_383_3_degree_pos : 0 < luebeckConwayPolynomial_383_3.degree

Positive degree of C(383, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_383_3 : luebeckConwayPolynomial? 383 3 = some luebeckConwayPolynomial_383_3

Lookup identifies the imported C(383, 3).

def Hex.Conway.luebeckConwayPolynomial_167_3 : FpPoly 167

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_167_3_monic : DensePoly.Monic luebeckConwayPolynomial_167_3

Monicity of C(167, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_167_3_degree_pos : 0 < luebeckConwayPolynomial_167_3.degree

Positive degree of C(167, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_167_3 : luebeckConwayPolynomial? 167 3 = some luebeckConwayPolynomial_167_3

Lookup identifies the imported C(167, 3).

def Hex.Conway.luebeckConwayPolynomial_73_3 : FpPoly 73

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_73_3_monic : DensePoly.Monic luebeckConwayPolynomial_73_3

Monicity of C(73, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_73_3_degree_pos : 0 < luebeckConwayPolynomial_73_3.degree

Positive degree of C(73, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_73_3 : luebeckConwayPolynomial? 73 3 = some luebeckConwayPolynomial_73_3

Lookup identifies the imported C(73, 3).

def Hex.Conway.luebeckConwayPolynomial_97_3 : FpPoly 97

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_97_3_monic : DensePoly.Monic luebeckConwayPolynomial_97_3

Monicity of C(97, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_97_3_degree_pos : 0 < luebeckConwayPolynomial_97_3.degree

Positive degree of C(97, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_97_3 : luebeckConwayPolynomial? 97 3 = some luebeckConwayPolynomial_97_3

Lookup identifies the imported C(97, 3).

def Hex.Conway.luebeckConwayPolynomial_31_3 : FpPoly 31

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_31_3_monic : DensePoly.Monic luebeckConwayPolynomial_31_3

Monicity of C(31, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_31_3_degree_pos : 0 < luebeckConwayPolynomial_31_3.degree

Positive degree of C(31, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_31_3 : luebeckConwayPolynomial? 31 3 = some luebeckConwayPolynomial_31_3

Lookup identifies the imported C(31, 3).

def Hex.Conway.luebeckConwayPolynomial_859_2 : FpPoly 859

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_859_2_monic : DensePoly.Monic luebeckConwayPolynomial_859_2

Monicity of C(859, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_859_2_degree_pos : 0 < luebeckConwayPolynomial_859_2.degree

Positive degree of C(859, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_859_2 : luebeckConwayPolynomial? 859 2 = some luebeckConwayPolynomial_859_2

Lookup identifies the imported C(859, 2).

def Hex.Conway.luebeckConwayPolynomial_461_2 : FpPoly 461

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_461_2_monic : DensePoly.Monic luebeckConwayPolynomial_461_2

Monicity of C(461, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_461_2_degree_pos : 0 < luebeckConwayPolynomial_461_2.degree

Positive degree of C(461, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_461_2 : luebeckConwayPolynomial? 461 2 = some luebeckConwayPolynomial_461_2

Lookup identifies the imported C(461, 2).

def Hex.Conway.luebeckConwayPolynomial_547_2 : FpPoly 547

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_547_2_monic : DensePoly.Monic luebeckConwayPolynomial_547_2

Monicity of C(547, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_547_2_degree_pos : 0 < luebeckConwayPolynomial_547_2.degree

Positive degree of C(547, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_547_2 : luebeckConwayPolynomial? 547 2 = some luebeckConwayPolynomial_547_2

Lookup identifies the imported C(547, 2).

def Hex.Conway.luebeckConwayPolynomial_617_2 : FpPoly 617

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_617_2_monic : DensePoly.Monic luebeckConwayPolynomial_617_2

Monicity of C(617, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_617_2_degree_pos : 0 < luebeckConwayPolynomial_617_2.degree

Positive degree of C(617, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_617_2 : luebeckConwayPolynomial? 617 2 = some luebeckConwayPolynomial_617_2

Lookup identifies the imported C(617, 2).

def Hex.Conway.luebeckConwayPolynomial_661_2 : FpPoly 661

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_661_2_monic : DensePoly.Monic luebeckConwayPolynomial_661_2

Monicity of C(661, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_661_2_degree_pos : 0 < luebeckConwayPolynomial_661_2.degree

Positive degree of C(661, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_661_2 : luebeckConwayPolynomial? 661 2 = some luebeckConwayPolynomial_661_2

Lookup identifies the imported C(661, 2).

def Hex.Conway.luebeckConwayPolynomial_709_2 : FpPoly 709

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_709_2_monic : DensePoly.Monic luebeckConwayPolynomial_709_2

Monicity of C(709, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_709_2_degree_pos : 0 < luebeckConwayPolynomial_709_2.degree

Positive degree of C(709, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_709_2 : luebeckConwayPolynomial? 709 2 = some luebeckConwayPolynomial_709_2

Lookup identifies the imported C(709, 2).

def Hex.Conway.luebeckConwayPolynomial_761_2 : FpPoly 761

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_761_2_monic : DensePoly.Monic luebeckConwayPolynomial_761_2

Monicity of C(761, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_761_2_degree_pos : 0 < luebeckConwayPolynomial_761_2.degree

Positive degree of C(761, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_761_2 : luebeckConwayPolynomial? 761 2 = some luebeckConwayPolynomial_761_2

Lookup identifies the imported C(761, 2).

def Hex.Conway.luebeckConwayPolynomial_821_2 : FpPoly 821

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_821_2_monic : DensePoly.Monic luebeckConwayPolynomial_821_2

Monicity of C(821, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_821_2_degree_pos : 0 < luebeckConwayPolynomial_821_2.degree

Positive degree of C(821, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_821_2 : luebeckConwayPolynomial? 821 2 = some luebeckConwayPolynomial_821_2

Lookup identifies the imported C(821, 2).

def Hex.Conway.luebeckConwayPolynomial_853_2 : FpPoly 853

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_853_2_monic : DensePoly.Monic luebeckConwayPolynomial_853_2

Monicity of C(853, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_853_2_degree_pos : 0 < luebeckConwayPolynomial_853_2.degree

Positive degree of C(853, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_853_2 : luebeckConwayPolynomial? 853 2 = some luebeckConwayPolynomial_853_2

Lookup identifies the imported C(853, 2).

def Hex.Conway.luebeckConwayPolynomial_919_2 : FpPoly 919

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_919_2_monic : DensePoly.Monic luebeckConwayPolynomial_919_2

Monicity of C(919, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_919_2_degree_pos : 0 < luebeckConwayPolynomial_919_2.degree

Positive degree of C(919, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_919_2 : luebeckConwayPolynomial? 919 2 = some luebeckConwayPolynomial_919_2

Lookup identifies the imported C(919, 2).