OAI/Geometry/SingularHomology/SingularChainsFinsupp.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem340.RealSingularSimplex line 12
  2. abbrev OAI.Problem340.RealSingularChains line 15
  3. def OAI.Problem340.simplicialChainsFinsuppEquiv line 18
  4. theorem OAI.Problem340.simplicialChainsFinsuppEquiv_single line 24
  5. def OAI.Problem340.singularChainsFinsuppEquiv line 33
  6. def OAI.Problem340.realSingularGenerator line 38
  7. theorem OAI.Problem340.singularChainsFinsuppEquiv_single line 44
  8. theorem OAI.Problem340.singularChainsFinsuppEquiv_symm_generator line 52
  9. def OAI.Problem340.realSingularChainBasis line 57
  10. theorem OAI.Problem340.realSingularChainBasis_apply line 62
  11. theorem OAI.Problem340.realSingularChain_linearMap_ext line 68
  12. theorem OAI.Problem340.realSingularChain_induction line 77
  13. def OAI.Problem340.realSingularChainLift line 89
  14. theorem OAI.Problem340.realSingularChainLift_generator line 95
  15. theorem OAI.Problem340.realSingularChainLift_unique line 103