OAI/Combinatorics/Progressions/Estimates/ProjectedTranslationGroup.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.PolynomialTranslationGroup.baseRangeGroup line 13
  2. theorem OAI.Erdos3.PolynomialTranslationGroup.mem_baseRangeGroup line 21
  3. def OAI.Erdos3.PolynomialTranslationGroup.projectedGroupBaseCoordinates line 25
  4. theorem OAI.Erdos3.PolynomialTranslationGroup.apply_projectedGroupBaseCoordinates line 31
  5. theorem OAI.Erdos3.PolynomialTranslationGroup.projectedGroupBaseCoordinates_one line 37
  6. theorem OAI.Erdos3.PolynomialTranslationGroup.projectedGroupBaseCoordinates_mul line 43
  7. def OAI.Erdos3.PolynomialTranslationGroup.projectedGroupRestriction line 50
  8. theorem OAI.Erdos3.PolynomialTranslationGroup.projectedGroupRestriction_base line 72
  9. theorem OAI.Erdos3.PolynomialTranslationGroup.projectedGroupRestriction_polynomial line 77
  10. theorem OAI.Erdos3.PolynomialTranslationGroup.projectedGroupRestriction_coeff_zero line 83
  11. theorem OAI.Erdos3.PolynomialTranslationGroup.projectedGroupRestriction_eval line 89
  12. theorem OAI.Erdos3.PolynomialTranslationGroup.exponentialElement_mem_baseRangeGroup line 96
  13. def OAI.Erdos3.PolynomialTranslationGroup.baseRangeExponentialElement line 100
  14. theorem OAI.Erdos3.PolynomialTranslationGroup.projectedGroupBaseCoordinates_exponentialElement line 104
  15. theorem OAI.Erdos3.PolynomialTranslationGroup.potentialElement_mem_baseRangeGroup line 113
  16. def OAI.Erdos3.PolynomialTranslationGroup.baseRangePotentialElement line 117
  17. theorem OAI.Erdos3.PolynomialTranslationGroup.projectedGroupRestriction_potentialElement line 121
  18. theorem OAI.Erdos3.PolynomialTranslationGroup.projectedGroupRestriction_exponentialElement line 134