OAI/NumberTheory/Jacobsthal/Harmonic/PrimitiveResultant.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Erdos970.ErdosBivariateResultant.Bivariate line 12
  2. def OAI.Erdos970.ErdosBivariateResultant.specialize line 14
  3. def OAI.Erdos970.ErdosBivariateResultant.pointEvalHom line 17
  4. def OAI.Erdos970.ErdosBivariateResultant.beval line 20
  5. def OAI.Erdos970.ErdosBivariateResultant.xResultant line 22
  6. theorem OAI.Erdos970.ErdosBivariateResultant.beval_eq_specialize line 24
  7. theorem OAI.Erdos970.ErdosBivariateResultant.beval_add line 27
  8. theorem OAI.Erdos970.ErdosBivariateResultant.beval_mul line 29
  9. theorem OAI.Erdos970.ErdosBivariateResultant.beval_C line 31
  10. theorem OAI.Erdos970.ErdosBivariateResultant.resultant_bezout line 35
  11. theorem OAI.Erdos970.ErdosBivariateResultant.common_zero_resultant_zero line 40
  12. theorem OAI.Erdos970.ErdosBivariateResultant.specialize_degree_le line 48
  13. theorem OAI.Erdos970.ErdosBivariateResultant.common_zero_resultant_zero_of_fiber line 51
  14. theorem OAI.Erdos970.ErdosBivariateResultant.determinant_degree_le line 68
  15. theorem OAI.Erdos970.ErdosBivariateResultant.resultant_degree_from_coefficients line 79
  16. def OAI.Erdos970.ErdosBivariateResultant.coefficientDegree line 102
  17. theorem OAI.Erdos970.ErdosBivariateResultant.coeff_degree_le line 105
  18. theorem OAI.Erdos970.ErdosBivariateResultant.xResultant_degree_le line 112
  19. theorem OAI.Erdos970.ErdosBivariateResultant.xResultant_degree_uniform line 117
  20. def OAI.Erdos970.ErdosBivariateResultant.resultantRoots line 136
  21. def OAI.Erdos970.ErdosBivariateResultant.verticalRoots line 137
  22. def OAI.Erdos970.ErdosBivariateResultant.rootPairs line 139
  23. def OAI.Erdos970.ErdosBivariateResultant.commonZeroFinset line 142
  24. def OAI.Erdos970.ErdosBivariateResultant.commonZeroSet line 145
  25. theorem OAI.Erdos970.ErdosBivariateResultant.mem_resultantRoots line 148
  26. theorem OAI.Erdos970.ErdosBivariateResultant.mem_verticalRoots line 152
  27. theorem OAI.Erdos970.ErdosBivariateResultant.mem_rootPairs line 157
  28. theorem OAI.Erdos970.ErdosBivariateResultant.mem_commonZeroFinset line 168
  29. theorem OAI.Erdos970.ErdosBivariateResultant.coe_commonZeroFinset line 180
  30. theorem OAI.Erdos970.ErdosBivariateResultant.commonZeroSet_finite line 186
  31. theorem OAI.Erdos970.ErdosBivariateResultant.resultantRoots_card_le line 191
  32. theorem OAI.Erdos970.ErdosBivariateResultant.verticalRoots_card_le line 195
  33. theorem OAI.Erdos970.ErdosBivariateResultant.commonZeroFinset_card_le line 198
  34. theorem OAI.Erdos970.ErdosBivariateResultant.common_zero_finite_count line 211
  35. theorem OAI.Erdos970.ErdosBivariateResultant.common_zero_count_coefficient_bound line 219
  36. theorem OAI.Erdos970.ErdosBivariateResultant.common_zero_count_uniform line 225
  37. def OAI.Erdos970.ErdosBivariateResultant.commonAbscissae line 245
  38. def OAI.Erdos970.ErdosBivariateResultant.commonVerticalRoots line 248
  39. theorem OAI.Erdos970.ErdosBivariateResultant.mem_commonAbscissae line 251
  40. theorem OAI.Erdos970.ErdosBivariateResultant.commonAbscissae_card_le line 263
  41. theorem OAI.Erdos970.ErdosBivariateResultant.mem_commonVerticalRoots line 271
  42. theorem OAI.Erdos970.ErdosBivariateResultant.commonVerticalRoots_card_le line 275
  43. theorem OAI.Erdos970.ErdosBivariateResultant.coe_commonZeroFinset_on_resultant line 279
  44. theorem OAI.Erdos970.ErdosBivariateResultant.common_zero_finite_count_on_resultant line 295
  45. theorem OAI.Erdos970.ErdosCriticalGeometry.primitive_specialize_ne_zero line 313
  46. theorem OAI.Erdos970.ErdosCriticalGeometry.irreducible_resultant_ne_zero line 328