OAI/Geometry/SingularHomology/SimplicialSphereHomology.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem340.SimplicialSphere.sphere line 11
  2. abbrev OAI.Problem340.SimplicialSphere.coefficients line 12
  3. abbrev OAI.Problem340.SimplicialSphere.chains line 13
  4. def OAI.Problem340.SimplicialSphere.face line 15
  5. lemma OAI.Problem340.SimplicialSphere.face_nondegenerate line 20
  6. def OAI.Problem340.SimplicialSphere.fundamentalCycle line 27
  7. lemma OAI.Problem340.SimplicialSphere.face_injective line 33
  8. lemma OAI.Problem340.SimplicialSphere.fundamentalCycle_boundary line 40
  9. def OAI.Problem340.SimplicialSphere.coefficient line 78
  10. lemma OAI.Problem340.SimplicialSphere.face_coefficient line 83
  11. lemma OAI.Problem340.SimplicialSphere.fundamentalCycle_coefficient line 94
  12. lemma OAI.Problem340.SimplicialSphere.fundamentalCycle_ne_zero line 101
  13. lemma OAI.Problem340.SimplicialSphere.incoming_differential_zero line 108
  14. theorem OAI.Problem340.SimplicialSphere.normalized_homology_two_not_isZero line 111
  15. theorem OAI.Problem340.SimplicialSphere.homology_two_not_isZero line 122
  16. theorem OAI.Problem340.SimplicialSphere.homology_two_nontrivial line 131