OAI/Geometry/SingularHomology/TetrahedronHomologyRank.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Problem340.SimplicialSphere.face_surjective line 12
  2. def OAI.Problem340.SimplicialSphere.faceEquiv line 28
  3. lemma OAI.Problem340.SimplicialSphere.card_nondegenerate_two line 32
  4. lemma OAI.Problem340.SimplicialSphere.face_coordinate_decomposition line 36
  5. lemma OAI.Problem340.SimplicialSphere.eq_zero_of_face_coordinates_eq_zero line 47
  6. lemma OAI.Problem340.SimplicialSphere.face_edge_nondegenerate line 52
  7. def OAI.Problem340.SimplicialSphere.edgeCoefficient line 60
  8. lemma OAI.Problem340.SimplicialSphere.face_edge_coefficient line 67
  9. lemma OAI.Problem340.SimplicialSphere.face_edge_eq_iff line 78
  10. lemma OAI.Problem340.SimplicialSphere.simplex_face_edge_eq_iff line 89
  11. lemma OAI.Problem340.SimplicialSphere.boundary_edge_zero line 95
  12. lemma OAI.Problem340.SimplicialSphere.boundary_edge_one line 108
  13. lemma OAI.Problem340.SimplicialSphere.boundary_edge_two line 121
  14. lemma OAI.Problem340.SimplicialSphere.cycle_eq_zero_of_first_coordinate line 134
  15. def OAI.Problem340.SimplicialSphere.firstCycleCoordinate line 150
  16. lemma OAI.Problem340.SimplicialSphere.firstCycleCoordinate_injective line 154
  17. lemma OAI.Problem340.SimplicialSphere.finrank_cycles_two_le_one line 161
  18. lemma OAI.Problem340.SimplicialSphere.finrank_normalized_homology_two_le_one line 164
  19. theorem OAI.Problem340.SimplicialSphere.finrank_homology_two line 177