OAI/Combinatorics/Progressions/Polynomial/UniformPolynomialPeriodBudget.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.polynomial_period_cost_le_exp line 13
  2. theorem OAI.Erdos3.exists_polynomial_BCH_period_exp_bound line 60
  3. theorem OAI.Erdos3.exists_factor_through_integer_reduction line 95
  4. theorem OAI.Erdos3.exists_polynomial_BCH_finite_quotient line 110
  5. theorem OAI.Erdos3.polynomialDenominator_dvd_power line 141
  6. theorem OAI.Erdos3.polynomialFamilyDenominator_dvd_power line 152
  7. def OAI.Erdos3.uniformPolynomialBCHPeriod line 164
  8. theorem OAI.Erdos3.uniformPolynomialBCHPeriod_pos line 168
  9. theorem OAI.Erdos3.polynomialBCHPeriod_dvd_uniform line 174
  10. theorem OAI.Erdos3.polynomialBCHMap_uniform_coset_eq line 182
  11. theorem OAI.Erdos3.polynomialBCHMap_uniform_inverse_coset_eq line 195
  12. theorem OAI.Erdos3.exists_real_polynomial_BCH_finite_quotient line 227
  13. theorem OAI.Erdos3.uniformPolynomialBCHPeriod_le_exp line 267
  14. theorem OAI.Erdos3.exists_uniformPolynomialBCHPeriod_exp_bound line 297
  15. theorem OAI.Erdos3.realPolynomialBCHMap_uniform_cosets line 313