OAI/Geometry/HeilbronnTriangle/ProportionalPairs.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem355.ProportionalPairs.proportional_parameter line 12
  2. theorem OAI.Problem355.ProportionalPairs.card_coordinate_pairs_le_gcd line 34
  3. theorem OAI.Problem355.ProportionalPairs.sum_gcd_sq_le_cube_of_subset line 62
  4. def OAI.Problem355.ProportionalPairs.coordinatePairs line 78
  5. def OAI.Problem355.ProportionalPairs.proportionalPairParameters line 81
  6. theorem OAI.Problem355.ProportionalPairs.card_proportionalPairParameters_le line 85
  7. abbrev OAI.Problem355.ProportionalPairs.NatColumn line 107
  8. def OAI.Problem355.ProportionalPairs.columnBox line 109
  9. def OAI.Problem355.ProportionalPairs.Proportional line 112
  10. instance OAI.Problem355.ProportionalPairs.(instance at line 115) line 115
  11. def OAI.Problem355.ProportionalPairs.proportionalPairs line 118
  12. theorem OAI.Problem355.ProportionalPairs.card_proportionalPairs_le line 121
  13. def OAI.Problem355.ProportionalPairs.project line 148
  14. theorem OAI.Problem355.ProportionalPairs.project_eq_iff_proportional line 151
  15. theorem OAI.Problem355.ProportionalPairs.card_equal_projection_pairs_le line 165
  16. theorem OAI.Problem355.ProportionalPairs.card_equal_projection_pairs_le_of_subset line 191
  17. theorem OAI.Problem355.ProportionalPairs.uniform_collision_fraction_le line 198