OAI/Combinatorics/Progressions/Estimates/NonprincipalDilation.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.nonprincipalCoefficientSlots line 11
  2. theorem OAI.Erdos3.mem_nonprincipalCoefficientSlots line 16
  3. theorem OAI.Erdos3.mem_monomialExponentSet line 23
  4. theorem OAI.Erdos3.mem_fixedNonprincipalExponents line 29
  5. theorem OAI.Erdos3.nonprincipalCoefficientSlots_image line 36
  6. theorem OAI.Erdos3.nonprincipalCoefficientSlots_sum line 53
  7. theorem OAI.Erdos3.nonprincipalCoefficientSlots_not_principal line 60
  8. theorem OAI.Erdos3.nonprincipalCoefficientSlots_not_zero line 69
  9. theorem OAI.Erdos3.nonprincipalCoefficientSlots_degree line 78
  10. def OAI.Erdos3.nonprincipalDilation line 92
  11. theorem OAI.Erdos3.nonprincipalDilation_principal line 97
  12. theorem OAI.Erdos3.nonprincipalDilation_zero line 103
  13. theorem OAI.Erdos3.nonprincipalDilation_mem line 109
  14. theorem OAI.Erdos3.nonprincipalDilation_pos line 115
  15. theorem OAI.Erdos3.nonprincipalDilation_le_one line 122
  16. theorem OAI.Erdos3.nonprincipalDilation_lower line 129