OAI/Geometry/SingularHomology/HomologyEvaluation.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem340.moduleHomologyEvaluation line 16
  2. theorem OAI.Problem340.moduleHomologyEvaluation_class line 26
  3. theorem OAI.Problem340.moduleHomologyClass_surjective line 35
  4. theorem OAI.Problem340.moduleHomologyClass_ne_zero_of_evaluation line 41
  5. theorem OAI.Problem340.moduleHomologyEvaluation_unique line 50
  6. theorem OAI.Problem340.moduleCycle_map line 61
  7. theorem OAI.Problem340.moduleHomologyEvaluation_naturality line 68
  8. def OAI.Problem340.realSingularHomologyEvaluation line 89
  9. def OAI.Problem340.positiveRealSingularCycleClass line 100
  10. theorem OAI.Problem340.realSingularHomologyEvaluation_cycleClass line 111
  11. theorem OAI.Problem340.positiveRealSingularCycleClass_ne_zero_of_evaluation line 122
  12. theorem OAI.Problem340.realSingularHomologyEvaluation_naturality line 134
  13. theorem OAI.Problem340.positiveRealSingularCycleClass_eq_zero_iff line 151