def Hex.Conway.luebeckConwayPolynomial_463_3 : FpPoly 463

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_463_3_monic : DensePoly.Monic luebeckConwayPolynomial_463_3

Monicity of C(463, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_463_3_degree_pos : 0 < luebeckConwayPolynomial_463_3.degree

Positive degree of C(463, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_463_3 : luebeckConwayPolynomial? 463 3 = some luebeckConwayPolynomial_463_3

Lookup identifies the imported C(463, 3).

def Hex.Conway.luebeckConwayPolynomial_541_3 : FpPoly 541

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_541_3_monic : DensePoly.Monic luebeckConwayPolynomial_541_3

Monicity of C(541, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_541_3_degree_pos : 0 < luebeckConwayPolynomial_541_3.degree

Positive degree of C(541, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_541_3 : luebeckConwayPolynomial? 541 3 = some luebeckConwayPolynomial_541_3

Lookup identifies the imported C(541, 3).

def Hex.Conway.luebeckConwayPolynomial_613_3 : FpPoly 613

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_613_3_monic : DensePoly.Monic luebeckConwayPolynomial_613_3

Monicity of C(613, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_613_3_degree_pos : 0 < luebeckConwayPolynomial_613_3.degree

Positive degree of C(613, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_613_3 : luebeckConwayPolynomial? 613 3 = some luebeckConwayPolynomial_613_3

Lookup identifies the imported C(613, 3).

def Hex.Conway.luebeckConwayPolynomial_647_3 : FpPoly 647

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_647_3_monic : DensePoly.Monic luebeckConwayPolynomial_647_3

Monicity of C(647, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_647_3_degree_pos : 0 < luebeckConwayPolynomial_647_3.degree

Positive degree of C(647, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_647_3 : luebeckConwayPolynomial? 647 3 = some luebeckConwayPolynomial_647_3

Lookup identifies the imported C(647, 3).

def Hex.Conway.luebeckConwayPolynomial_683_3 : FpPoly 683

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_683_3_monic : DensePoly.Monic luebeckConwayPolynomial_683_3

Monicity of C(683, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_683_3_degree_pos : 0 < luebeckConwayPolynomial_683_3.degree

Positive degree of C(683, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_683_3 : luebeckConwayPolynomial? 683 3 = some luebeckConwayPolynomial_683_3

Lookup identifies the imported C(683, 3).

def Hex.Conway.luebeckConwayPolynomial_751_3 : FpPoly 751

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_751_3_monic : DensePoly.Monic luebeckConwayPolynomial_751_3

Monicity of C(751, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_751_3_degree_pos : 0 < luebeckConwayPolynomial_751_3.degree

Positive degree of C(751, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_751_3 : luebeckConwayPolynomial? 751 3 = some luebeckConwayPolynomial_751_3

Lookup identifies the imported C(751, 3).

def Hex.Conway.luebeckConwayPolynomial_853_3 : FpPoly 853

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_853_3_monic : DensePoly.Monic luebeckConwayPolynomial_853_3

Monicity of C(853, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_853_3_degree_pos : 0 < luebeckConwayPolynomial_853_3.degree

Positive degree of C(853, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_853_3 : luebeckConwayPolynomial? 853 3 = some luebeckConwayPolynomial_853_3

Lookup identifies the imported C(853, 3).

def Hex.Conway.luebeckConwayPolynomial_911_3 : FpPoly 911

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_911_3_monic : DensePoly.Monic luebeckConwayPolynomial_911_3

Monicity of C(911, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_911_3_degree_pos : 0 < luebeckConwayPolynomial_911_3.degree

Positive degree of C(911, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_911_3 : luebeckConwayPolynomial? 911 3 = some luebeckConwayPolynomial_911_3

Lookup identifies the imported C(911, 3).

def Hex.Conway.luebeckConwayPolynomial_191_3 : FpPoly 191

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_191_3_monic : DensePoly.Monic luebeckConwayPolynomial_191_3

Monicity of C(191, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_191_3_degree_pos : 0 < luebeckConwayPolynomial_191_3.degree

Positive degree of C(191, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_191_3 : luebeckConwayPolynomial? 191 3 = some luebeckConwayPolynomial_191_3

Lookup identifies the imported C(191, 3).

def Hex.Conway.luebeckConwayPolynomial_263_3 : FpPoly 263

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_263_3_monic : DensePoly.Monic luebeckConwayPolynomial_263_3

Monicity of C(263, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_263_3_degree_pos : 0 < luebeckConwayPolynomial_263_3.degree

Positive degree of C(263, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_263_3 : luebeckConwayPolynomial? 263 3 = some luebeckConwayPolynomial_263_3

Lookup identifies the imported C(263, 3).

def Hex.Conway.luebeckConwayPolynomial_307_3 : FpPoly 307

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_307_3_monic : DensePoly.Monic luebeckConwayPolynomial_307_3

Monicity of C(307, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_307_3_degree_pos : 0 < luebeckConwayPolynomial_307_3.degree

Positive degree of C(307, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_307_3 : luebeckConwayPolynomial? 307 3 = some luebeckConwayPolynomial_307_3

Lookup identifies the imported C(307, 3).

def Hex.Conway.luebeckConwayPolynomial_349_3 : FpPoly 349

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_349_3_monic : DensePoly.Monic luebeckConwayPolynomial_349_3

Monicity of C(349, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_349_3_degree_pos : 0 < luebeckConwayPolynomial_349_3.degree

Positive degree of C(349, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_349_3 : luebeckConwayPolynomial? 349 3 = some luebeckConwayPolynomial_349_3

Lookup identifies the imported C(349, 3).

def Hex.Conway.luebeckConwayPolynomial_397_3 : FpPoly 397

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_397_3_monic : DensePoly.Monic luebeckConwayPolynomial_397_3

Monicity of C(397, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_397_3_degree_pos : 0 < luebeckConwayPolynomial_397_3.degree

Positive degree of C(397, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_397_3 : luebeckConwayPolynomial? 397 3 = some luebeckConwayPolynomial_397_3

Lookup identifies the imported C(397, 3).

def Hex.Conway.luebeckConwayPolynomial_443_3 : FpPoly 443

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_443_3_monic : DensePoly.Monic luebeckConwayPolynomial_443_3

Monicity of C(443, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_443_3_degree_pos : 0 < luebeckConwayPolynomial_443_3.degree

Positive degree of C(443, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_443_3 : luebeckConwayPolynomial? 443 3 = some luebeckConwayPolynomial_443_3

Lookup identifies the imported C(443, 3).

def Hex.Conway.luebeckConwayPolynomial_499_3 : FpPoly 499

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_499_3_monic : DensePoly.Monic luebeckConwayPolynomial_499_3

Monicity of C(499, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_499_3_degree_pos : 0 < luebeckConwayPolynomial_499_3.degree

Positive degree of C(499, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_499_3 : luebeckConwayPolynomial? 499 3 = some luebeckConwayPolynomial_499_3

Lookup identifies the imported C(499, 3).

def Hex.Conway.luebeckConwayPolynomial_139_3 : FpPoly 139

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_139_3_monic : DensePoly.Monic luebeckConwayPolynomial_139_3

Monicity of C(139, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_139_3_degree_pos : 0 < luebeckConwayPolynomial_139_3.degree

Positive degree of C(139, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_139_3 : luebeckConwayPolynomial? 139 3 = some luebeckConwayPolynomial_139_3

Lookup identifies the imported C(139, 3).

def Hex.Conway.luebeckConwayPolynomial_181_3 : FpPoly 181

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_181_3_monic : DensePoly.Monic luebeckConwayPolynomial_181_3

Monicity of C(181, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_181_3_degree_pos : 0 < luebeckConwayPolynomial_181_3.degree

Positive degree of C(181, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_181_3 : luebeckConwayPolynomial? 181 3 = some luebeckConwayPolynomial_181_3

Lookup identifies the imported C(181, 3).

def Hex.Conway.luebeckConwayPolynomial_563_3 : FpPoly 563

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_563_3_monic : DensePoly.Monic luebeckConwayPolynomial_563_3

Monicity of C(563, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_563_3_degree_pos : 0 < luebeckConwayPolynomial_563_3.degree

Positive degree of C(563, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_563_3 : luebeckConwayPolynomial? 563 3 = some luebeckConwayPolynomial_563_3

Lookup identifies the imported C(563, 3).

def Hex.Conway.luebeckConwayPolynomial_593_3 : FpPoly 593

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_593_3_monic : DensePoly.Monic luebeckConwayPolynomial_593_3

Monicity of C(593, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_593_3_degree_pos : 0 < luebeckConwayPolynomial_593_3.degree

Positive degree of C(593, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_593_3 : luebeckConwayPolynomial? 593 3 = some luebeckConwayPolynomial_593_3

Lookup identifies the imported C(593, 3).

def Hex.Conway.luebeckConwayPolynomial_719_3 : FpPoly 719

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_719_3_monic : DensePoly.Monic luebeckConwayPolynomial_719_3

Monicity of C(719, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_719_3_degree_pos : 0 < luebeckConwayPolynomial_719_3.degree

Positive degree of C(719, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_719_3 : luebeckConwayPolynomial? 719 3 = some luebeckConwayPolynomial_719_3

Lookup identifies the imported C(719, 3).

def Hex.Conway.luebeckConwayPolynomial_769_3 : FpPoly 769

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_769_3_monic : DensePoly.Monic luebeckConwayPolynomial_769_3

Monicity of C(769, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_769_3_degree_pos : 0 < luebeckConwayPolynomial_769_3.degree

Positive degree of C(769, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_769_3 : luebeckConwayPolynomial? 769 3 = some luebeckConwayPolynomial_769_3

Lookup identifies the imported C(769, 3).

def Hex.Conway.luebeckConwayPolynomial_883_3 : FpPoly 883

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_883_3_monic : DensePoly.Monic luebeckConwayPolynomial_883_3

Monicity of C(883, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_883_3_degree_pos : 0 < luebeckConwayPolynomial_883_3.degree

Positive degree of C(883, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_883_3 : luebeckConwayPolynomial? 883 3 = some luebeckConwayPolynomial_883_3

Lookup identifies the imported C(883, 3).

def Hex.Conway.luebeckConwayPolynomial_977_3 : FpPoly 977

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_977_3_monic : DensePoly.Monic luebeckConwayPolynomial_977_3

Monicity of C(977, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_977_3_degree_pos : 0 < luebeckConwayPolynomial_977_3.degree

Positive degree of C(977, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_977_3 : luebeckConwayPolynomial? 977 3 = some luebeckConwayPolynomial_977_3

Lookup identifies the imported C(977, 3).

def Hex.Conway.luebeckConwayPolynomial_313_3 : FpPoly 313

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

Equations

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

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_313_3_monic : DensePoly.Monic luebeckConwayPolynomial_313_3

Monicity of C(313, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial_313_3_degree_pos : 0 < luebeckConwayPolynomial_313_3.degree

Positive degree of C(313, 3).

@[simp]

theorem Hex.Conway.luebeckConwayPolynomial?_hit_313_3 : luebeckConwayPolynomial? 313 3 = some luebeckConwayPolynomial_313_3

Lookup identifies the imported C(313, 3).