OAI/Combinatorics/Progressions/Lattices/TranslationIntegerReduction.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.integerFloorPolynomial line 16
  2. theorem OAI.Erdos3.coeff_integerFloorPolynomial line 19
  3. theorem OAI.Erdos3.integerFloorPolynomial_support_subset line 29
  4. theorem OAI.Erdos3.integerFloorPolynomial_mem_weightedSupportLT line 37
  5. theorem OAI.Erdos3.polynomialTranslate_mem_weightedSupportLT line 42
  6. def OAI.Erdos3.PolynomialTranslationGroupOver.integerReduction line 52
  7. theorem OAI.Erdos3.PolynomialTranslationGroupOver.integerReduction_base line 58
  8. theorem OAI.Erdos3.PolynomialTranslationGroupOver.integerReduction_product_base line 61
  9. theorem OAI.Erdos3.PolynomialTranslationGroupOver.integerReduction_product_polynomial line 67
  10. theorem OAI.Erdos3.PolynomialTranslationGroupOver.integerReduction_product_coefficient line 76
  11. theorem OAI.Erdos3.PolynomialTranslationGroupOver.integerReduction_product_bounds line 84
  12. theorem OAI.Erdos3.PolynomialTranslationGroupOver.integerReduction_weightedSupportLT line 97
  13. theorem OAI.Erdos3.PolynomialTranslationGroupOver.exists_integer_reduction line 110