OAI/Combinatorics/Progressions/Linear/FiniteRankTriangularFinset.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.finiteRankCorrectionSolutions line 12
  2. theorem OAI.Erdos3.finiteRankCorrectionSolutions_reindex line 19
  3. theorem OAI.Erdos3.exists_rank_triangular_equiv line 48
  4. theorem OAI.Erdos3.exists_finite_rank_triangular_correction_enumeration line 60
  5. theorem OAI.Erdos3.exists_finite_rank_triangular_correction_enumeration_exp line 91
  6. theorem OAI.Erdos3.exists_uniform_finite_rank_triangular_correction_enumeration line 108
  7. theorem OAI.Erdos3.correction_finset_of_enumeration line 142
  8. theorem OAI.Erdos3.exists_finite_rank_triangular_correction_finset line 162
  9. theorem OAI.Erdos3.exists_finite_rank_triangular_correction_finset_exp line 175
  10. theorem OAI.Erdos3.exists_uniform_finite_rank_triangular_correction_finset line 191