OAI/Combinatorics/Progressions/Estimates/TruncatedSeries.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.truncatedSeriesCon line 13
  2. abbrev OAI.Erdos3.TruncatedSeries line 25
  3. def OAI.Erdos3.truncatedSeriesMk line 27
  4. theorem OAI.Erdos3.truncatedSeriesMk_surjective line 30
  5. theorem OAI.Erdos3.truncatedSeriesMk_eq_iff line 34
  6. def OAI.Erdos3.truncatedSeriesCoeff line 39
  7. theorem OAI.Erdos3.truncatedSeriesCoeff_mk line 50
  8. theorem OAI.Erdos3.truncatedSeries_ext line 53
  9. def OAI.Erdos3.seriesConstantCoeff line 60
  10. def OAI.Erdos3.truncatedSeriesConstantCoeff line 66
  11. theorem OAI.Erdos3.truncatedSeriesConstantCoeff_mk line 72
  12. def OAI.Erdos3.truncatedSeriesMap line 75
  13. theorem OAI.Erdos3.truncatedSeriesMap_mk line 84
  14. theorem OAI.Erdos3.truncatedSeriesCoeff_map line 88
  15. theorem OAI.Erdos3.truncatedSeriesConstantCoeff_map line 95
  16. def OAI.Erdos3.truncatedSeriesPositive line 105
  17. theorem OAI.Erdos3.mem_truncatedSeriesPositive line 118
  18. theorem OAI.Erdos3.truncatedSeriesPositive_pow line 121
  19. theorem OAI.Erdos3.truncatedSeriesPositive_nilpotent line 133
  20. theorem OAI.Erdos3.truncatedSeriesMap_positive line 137