OAI/Combinatorics/Progressions/Polynomial/PolynomialCoefficientGridDenominator.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.integralRealPolynomialSubring line 19
  2. def OAI.Erdos3.realPolynomialCoefficientGrid line 22
  3. theorem OAI.Erdos3.mem_integralRealPolynomialSubring_iff line 25
  4. theorem OAI.Erdos3.C_int_mem_integralRealPolynomialSubring line 37
  5. theorem OAI.Erdos3.X_mem_integralRealPolynomialSubring line 41
  6. theorem OAI.Erdos3.rename_mem_integralRealPolynomialSubring line 45
  7. theorem OAI.Erdos3.realPolynomialCoefficientGrid_iff line 51
  8. theorem OAI.Erdos3.realPolynomialCoefficientGrid_add line 63
  9. theorem OAI.Erdos3.realPolynomialCoefficientGrid_neg line 72
  10. theorem OAI.Erdos3.realPolynomialCoefficientGrid_X line 79
  11. theorem OAI.Erdos3.realPolynomialCoefficientGrid_rename line 86
  12. theorem OAI.Erdos3.realPolynomialCoefficientGrid_mono line 93
  13. def OAI.Erdos3.majorShiftCoordinates line 116
  14. def OAI.Erdos3.majorShiftSubstitution line 120
  15. def OAI.Erdos3.majorSlowPolynomial line 124
  16. def OAI.Erdos3.majorRationalPolynomial line 130
  17. theorem OAI.Erdos3.majorShiftCoordinates_map line 135
  18. theorem OAI.Erdos3.majorRationalPolynomial_map line 141
  19. theorem OAI.Erdos3.majorShiftCoordinates_eval₂ line 152
  20. theorem OAI.Erdos3.majorShiftSubstitution_eval₂ line 159
  21. theorem OAI.Erdos3.majorSlowPolynomial_eval₂ line 166
  22. theorem OAI.Erdos3.majorRationalPolynomial_eval₂ line 177
  23. theorem OAI.Erdos3.majorShiftCoordinates_eval line 186
  24. theorem OAI.Erdos3.majorShiftSubstitution_eval line 191
  25. theorem OAI.Erdos3.majorSlowPolynomial_eval line 197
  26. theorem OAI.Erdos3.majorRationalPolynomial_eval line 214
  27. theorem OAI.Erdos3.majorShiftCoordinates_mass_le line 226
  28. theorem OAI.Erdos3.majorShiftSubstitution_mass_le line 233
  29. theorem OAI.Erdos3.majorSlowPolynomial_mass_le line 244
  30. theorem OAI.Erdos3.VectorPolynomial.coefficients_ofCoordinates_basisFun line 272
  31. theorem OAI.Erdos3.VectorPolynomial.coefficients_ofCoordinates_mem_realDenominatorGrid line 281
  32. theorem OAI.Erdos3.VectorPolynomial.coefficients_ofCoordinates_slowBound line 294
  33. theorem OAI.Erdos3.polynomial_substitution_totalDegree_le_ring line 315
  34. theorem OAI.Erdos3.variable_totalDegree_le_one line 332
  35. theorem OAI.Erdos3.majorShiftCoordinates_totalDegree_le line 343
  36. theorem OAI.Erdos3.majorShiftSubstitution_totalDegree_le line 349
  37. theorem OAI.Erdos3.majorSlowPolynomial_totalDegree_le line 356
  38. theorem OAI.Erdos3.majorRationalPolynomial_totalDegree_le line 373
  39. theorem OAI.Erdos3.majorSlowPolynomial_totalDegree_le_square line 387
  40. theorem OAI.Erdos3.majorRationalPolynomial_totalDegree_le_square line 399
  41. theorem OAI.Erdos3.cleared_substitution_term line 423
  42. theorem OAI.Erdos3.polynomial_substitution_cleared_mem line 445
  43. theorem OAI.Erdos3.realPolynomialCoefficientGrid_substitute line 465
  44. theorem OAI.Erdos3.realPolynomialCoefficientGrid_substitute_common line 482
  45. theorem OAI.Erdos3.majorShiftCoordinates_coefficientGrid line 491
  46. theorem OAI.Erdos3.majorRationalPolynomial_coefficientGrid line 498
  47. theorem OAI.Erdos3.realPolynomialCoefficientGrid_ratCast_iff line 513
  48. theorem OAI.Erdos3.majorRationalPolynomial_denominatorGrid line 520
  49. theorem OAI.Erdos3.realPolynomialCoefficientGrid_aeval_integral line 552
  50. theorem OAI.Erdos3.realPolynomialCoefficientGrid_intCast line 560
  51. theorem OAI.Erdos3.realPolynomialCoefficientGrid_integral_aeval line 566
  52. theorem OAI.Erdos3.realPolynomialCoefficientGrid_intCast_aeval line 577
  53. theorem OAI.Erdos3.realPolynomialCoefficientGrid_weightedHomogeneousComponent line 584
  54. theorem OAI.Erdos3.den_dvd_of_mem_denominatorGrid line 606
  55. theorem OAI.Erdos3.den_le_of_mem_denominatorGrid line 615
  56. theorem OAI.Erdos3.coeff_den_dvd_of_realPolynomialCoefficientGrid line 620
  57. theorem OAI.Erdos3.coeff_den_le_of_realPolynomialCoefficientGrid line 627