OAI/Combinatorics/Progressions/Estimates/RationalImageIntersections.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.kernel_equations_of_transpose_kernel line 16
  2. theorem OAI.Erdos3.exists_bounded_image_equations line 52
  3. theorem OAI.Erdos3.rationalKernelHeight_pos line 64
  4. theorem OAI.Erdos3.exists_bounded_quotient_presentation line 71
  5. def OAI.Erdos3.rationalQuotientEquiv line 87
  6. theorem OAI.Erdos3.rationalQuotientEquiv_apply_mk line 95
  7. theorem OAI.Erdos3.rationalQuotientEquiv_symm_apply line 104
  8. theorem OAI.Erdos3.rationalSolveHeight_mono line 123
  9. theorem OAI.Erdos3.rationalKernelHeight_mono line 133
  10. theorem OAI.Erdos3.exists_bounded_image_intersection_basis line 157
  11. theorem OAI.Erdos3.exists_image_intersection_basis_exp_height line 188