def Hex.Conway.luebeckConwayPolynomial_7_3 : FpPoly 7

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_7_3_monic : DensePoly.Monic luebeckConwayPolynomial_7_3

Monicity of C(7, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_7_3_degree_pos : 0 < luebeckConwayPolynomial_7_3.degree

Positive degree of C(7, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_7_3 : luebeckConwayPolynomial? 7 3 = some luebeckConwayPolynomial_7_3

Lookup identifies the imported C(7, 3).

def Hex.Conway.luebeckConwayPolynomial_863_2 : FpPoly 863

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_863_2_monic : DensePoly.Monic luebeckConwayPolynomial_863_2

Monicity of C(863, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_863_2_degree_pos : 0 < luebeckConwayPolynomial_863_2.degree

Positive degree of C(863, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_863_2 : luebeckConwayPolynomial? 863 2 = some luebeckConwayPolynomial_863_2

Lookup identifies the imported C(863, 2).

def Hex.Conway.luebeckConwayPolynomial_103_2 : FpPoly 103

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_103_2_monic : DensePoly.Monic luebeckConwayPolynomial_103_2

Monicity of C(103, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_103_2_degree_pos : 0 < luebeckConwayPolynomial_103_2.degree

Positive degree of C(103, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_103_2 : luebeckConwayPolynomial? 103 2 = some luebeckConwayPolynomial_103_2

Lookup identifies the imported C(103, 2).

def Hex.Conway.luebeckConwayPolynomial_383_2 : FpPoly 383

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_383_2_monic : DensePoly.Monic luebeckConwayPolynomial_383_2

Monicity of C(383, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_383_2_degree_pos : 0 < luebeckConwayPolynomial_383_2.degree

Positive degree of C(383, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_383_2 : luebeckConwayPolynomial? 383 2 = some luebeckConwayPolynomial_383_2

Lookup identifies the imported C(383, 2).

def Hex.Conway.luebeckConwayPolynomial_59_2 : FpPoly 59

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_59_2_monic : DensePoly.Monic luebeckConwayPolynomial_59_2

Monicity of C(59, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_59_2_degree_pos : 0 < luebeckConwayPolynomial_59_2.degree

Positive degree of C(59, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_59_2 : luebeckConwayPolynomial? 59 2 = some luebeckConwayPolynomial_59_2

Lookup identifies the imported C(59, 2).

def Hex.Conway.luebeckConwayPolynomial_193_2 : FpPoly 193

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_193_2_monic : DensePoly.Monic luebeckConwayPolynomial_193_2

Monicity of C(193, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_193_2_degree_pos : 0 < luebeckConwayPolynomial_193_2.degree

Positive degree of C(193, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_193_2 : luebeckConwayPolynomial? 193 2 = some luebeckConwayPolynomial_193_2

Lookup identifies the imported C(193, 2).

def Hex.Conway.luebeckConwayPolynomial_5_3 : FpPoly 5

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_5_3_monic : DensePoly.Monic luebeckConwayPolynomial_5_3

Monicity of C(5, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_5_3_degree_pos : 0 < luebeckConwayPolynomial_5_3.degree

Positive degree of C(5, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_5_3 : luebeckConwayPolynomial? 5 3 = some luebeckConwayPolynomial_5_3

Lookup identifies the imported C(5, 3).

def Hex.Conway.luebeckConwayPolynomial_37_2 : FpPoly 37

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_37_2_monic : DensePoly.Monic luebeckConwayPolynomial_37_2

Monicity of C(37, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_37_2_degree_pos : 0 < luebeckConwayPolynomial_37_2.degree

Positive degree of C(37, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_37_2 : luebeckConwayPolynomial? 37 2 = some luebeckConwayPolynomial_37_2

Lookup identifies the imported C(37, 2).

def Hex.Conway.luebeckConwayPolynomial_19_2 : FpPoly 19

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_19_2_monic : DensePoly.Monic luebeckConwayPolynomial_19_2

Monicity of C(19, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_19_2_degree_pos : 0 < luebeckConwayPolynomial_19_2.degree

Positive degree of C(19, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_19_2 : luebeckConwayPolynomial? 19 2 = some luebeckConwayPolynomial_19_2

Lookup identifies the imported C(19, 2).

def Hex.Conway.luebeckConwayPolynomial_11_2 : FpPoly 11

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_11_2_monic : DensePoly.Monic luebeckConwayPolynomial_11_2

Monicity of C(11, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_11_2_degree_pos : 0 < luebeckConwayPolynomial_11_2.degree

Positive degree of C(11, 2).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_11_2 : luebeckConwayPolynomial? 11 2 = some luebeckConwayPolynomial_11_2

Lookup identifies the imported C(11, 2).

def Hex.Conway.luebeckConwayPolynomial_547_1 : FpPoly 547

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_547_1_monic : DensePoly.Monic luebeckConwayPolynomial_547_1

Monicity of C(547, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_547_1_degree_pos : 0 < luebeckConwayPolynomial_547_1.degree

Positive degree of C(547, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_547_1 : luebeckConwayPolynomial? 547 1 = some luebeckConwayPolynomial_547_1

Lookup identifies the imported C(547, 1).

def Hex.Conway.luebeckConwayPolynomial_691_1 : FpPoly 691

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_691_1_monic : DensePoly.Monic luebeckConwayPolynomial_691_1

Monicity of C(691, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_691_1_degree_pos : 0 < luebeckConwayPolynomial_691_1.degree

Positive degree of C(691, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_691_1 : luebeckConwayPolynomial? 691 1 = some luebeckConwayPolynomial_691_1

Lookup identifies the imported C(691, 1).

def Hex.Conway.luebeckConwayPolynomial_991_1 : FpPoly 991

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_991_1_monic : DensePoly.Monic luebeckConwayPolynomial_991_1

Monicity of C(991, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_991_1_degree_pos : 0 < luebeckConwayPolynomial_991_1.degree

Positive degree of C(991, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_991_1 : luebeckConwayPolynomial? 991 1 = some luebeckConwayPolynomial_991_1

Lookup identifies the imported C(991, 1).

def Hex.Conway.luebeckConwayPolynomial_521_1 : FpPoly 521

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_521_1_monic : DensePoly.Monic luebeckConwayPolynomial_521_1

Monicity of C(521, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_521_1_degree_pos : 0 < luebeckConwayPolynomial_521_1.degree

Positive degree of C(521, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_521_1 : luebeckConwayPolynomial? 521 1 = some luebeckConwayPolynomial_521_1

Lookup identifies the imported C(521, 1).

def Hex.Conway.luebeckConwayPolynomial_599_1 : FpPoly 599

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_599_1_monic : DensePoly.Monic luebeckConwayPolynomial_599_1

Monicity of C(599, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_599_1_degree_pos : 0 < luebeckConwayPolynomial_599_1.degree

Positive degree of C(599, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_599_1 : luebeckConwayPolynomial? 599 1 = some luebeckConwayPolynomial_599_1

Lookup identifies the imported C(599, 1).

def Hex.Conway.luebeckConwayPolynomial_617_1 : FpPoly 617

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_617_1_monic : DensePoly.Monic luebeckConwayPolynomial_617_1

Monicity of C(617, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_617_1_degree_pos : 0 < luebeckConwayPolynomial_617_1.degree

Positive degree of C(617, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_617_1 : luebeckConwayPolynomial? 617 1 = some luebeckConwayPolynomial_617_1

Lookup identifies the imported C(617, 1).

def Hex.Conway.luebeckConwayPolynomial_659_1 : FpPoly 659

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_659_1_monic : DensePoly.Monic luebeckConwayPolynomial_659_1

Monicity of C(659, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_659_1_degree_pos : 0 < luebeckConwayPolynomial_659_1.degree

Positive degree of C(659, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_659_1 : luebeckConwayPolynomial? 659 1 = some luebeckConwayPolynomial_659_1

Lookup identifies the imported C(659, 1).

def Hex.Conway.luebeckConwayPolynomial_709_1 : FpPoly 709

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_709_1_monic : DensePoly.Monic luebeckConwayPolynomial_709_1

Monicity of C(709, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_709_1_degree_pos : 0 < luebeckConwayPolynomial_709_1.degree

Positive degree of C(709, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_709_1 : luebeckConwayPolynomial? 709 1 = some luebeckConwayPolynomial_709_1

Lookup identifies the imported C(709, 1).

def Hex.Conway.luebeckConwayPolynomial_743_1 : FpPoly 743

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_743_1_monic : DensePoly.Monic luebeckConwayPolynomial_743_1

Monicity of C(743, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_743_1_degree_pos : 0 < luebeckConwayPolynomial_743_1.degree

Positive degree of C(743, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_743_1 : luebeckConwayPolynomial? 743 1 = some luebeckConwayPolynomial_743_1

Lookup identifies the imported C(743, 1).

def Hex.Conway.luebeckConwayPolynomial_787_1 : FpPoly 787

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_787_1_monic : DensePoly.Monic luebeckConwayPolynomial_787_1

Monicity of C(787, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_787_1_degree_pos : 0 < luebeckConwayPolynomial_787_1.degree

Positive degree of C(787, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_787_1 : luebeckConwayPolynomial? 787 1 = some luebeckConwayPolynomial_787_1

Lookup identifies the imported C(787, 1).

def Hex.Conway.luebeckConwayPolynomial_827_1 : FpPoly 827

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_827_1_monic : DensePoly.Monic luebeckConwayPolynomial_827_1

Monicity of C(827, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_827_1_degree_pos : 0 < luebeckConwayPolynomial_827_1.degree

Positive degree of C(827, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_827_1 : luebeckConwayPolynomial? 827 1 = some luebeckConwayPolynomial_827_1

Lookup identifies the imported C(827, 1).

def Hex.Conway.luebeckConwayPolynomial_881_1 : FpPoly 881

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_881_1_monic : DensePoly.Monic luebeckConwayPolynomial_881_1

Monicity of C(881, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_881_1_degree_pos : 0 < luebeckConwayPolynomial_881_1.degree

Positive degree of C(881, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_881_1 : luebeckConwayPolynomial? 881 1 = some luebeckConwayPolynomial_881_1

Lookup identifies the imported C(881, 1).

def Hex.Conway.luebeckConwayPolynomial_937_1 : FpPoly 937

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_937_1_monic : DensePoly.Monic luebeckConwayPolynomial_937_1

Monicity of C(937, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_937_1_degree_pos : 0 < luebeckConwayPolynomial_937_1.degree

Positive degree of C(937, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_937_1 : luebeckConwayPolynomial? 937 1 = some luebeckConwayPolynomial_937_1

Lookup identifies the imported C(937, 1).

def Hex.Conway.luebeckConwayPolynomial_971_1 : FpPoly 971

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_971_1_monic : DensePoly.Monic luebeckConwayPolynomial_971_1

Monicity of C(971, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_971_1_degree_pos : 0 < luebeckConwayPolynomial_971_1.degree

Positive degree of C(971, 1).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_971_1 : luebeckConwayPolynomial? 971 1 = some luebeckConwayPolynomial_971_1

Lookup identifies the imported C(971, 1).