OAI/Combinatorics/RamseyFive/Geometry/SplitEquiv.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpRamseyFive.AffineChart.splitEquiv line 19
  2. theorem OAI.SharpRamseyFive.AffineChart.exists_coordinates_of_vectors line 38
  3. theorem OAI.SharpRamseyFive.AffineChart.exists_coordinates line 54
  4. def OAI.SharpRamseyFive.AffineChart.normalize line 63
  5. lemma OAI.SharpRamseyFive.AffineChart.lift_normalize line 65
  6. lemma OAI.SharpRamseyFive.AffineChart.reconstruct line 69
  7. lemma OAI.SharpRamseyFive.AffineChart.normalize_eq_iff line 73
  8. def OAI.SharpRamseyFive.AffineChart.point line 82
  9. lemma OAI.SharpRamseyFive.AffineChart.point_injective_on line 85
  10. theorem OAI.SharpRamseyFive.ProjectiveReduction.exists_projection_preserving_ranks line 99
  11. lemma OAI.SharpRamseyFive.ScalarExtension.coordinateMap_mem_span line 122
  12. theorem OAI.SharpRamseyFive.ScalarExtension.finrank_span_range line 133