OAI/Combinatorics/Progressions/Estimates/RationalHeight.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.RationalHeightLE line 13
  2. theorem OAI.Erdos3.RationalHeightLE.mono line 16
  3. theorem OAI.Erdos3.rational_fraction_entries_le line 20
  4. theorem OAI.Erdos3.rationalHeightLE_fraction line 37
  5. def OAI.Erdos3.arrayDenominator line 47
  6. def OAI.Erdos3.clearedArray line 49
  7. theorem OAI.Erdos3.arrayDenominator_pos line 53
  8. theorem OAI.Erdos3.arrayDenominator_le line 57
  9. theorem OAI.Erdos3.arrayDenominator_eq line 62
  10. theorem OAI.Erdos3.clearedArray_cast line 66
  11. theorem OAI.Erdos3.clearedArray_natAbs_le line 76
  12. theorem OAI.Erdos3.exists_bounded_integer_array line 91