OAI/Algebra/AuslanderReiten/Cones/TwoCone.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.ArExplicit.TwoCone.Data line 19
  2. abbrev OAI.ArExplicit.TwoCone.firstTerm line 32
  3. def OAI.ArExplicit.TwoCone.firstD line 35
  4. def OAI.ArExplicit.TwoCone.secondOnFirst line 38
  5. theorem OAI.ArExplicit.TwoCone.firstD_square line 41
  6. theorem OAI.ArExplicit.TwoCone.secondOnFirst_comm line 44
  7. abbrev OAI.ArExplicit.TwoCone.term line 61
  8. def OAI.ArExplicit.TwoCone.d line 64
  9. theorem OAI.ArExplicit.TwoCone.d_square line 67
  10. def OAI.ArExplicit.TwoCone.complex line 71
  11. theorem OAI.ArExplicit.TwoCone.firstD_exact line 75
  12. theorem OAI.ArExplicit.TwoCone.d_exact line 79
  13. theorem OAI.ArExplicit.TwoCone.complex_exactAt_succ line 84
  14. theorem OAI.ArExplicit.TwoCone.term_finite line 94
  15. theorem OAI.ArExplicit.TwoCone.term_projective line 102
  16. abbrev OAI.ArExplicit.TwoCone.Cokernel line 110
  17. abbrev OAI.ArExplicit.TwoCone.Cā‚ line 112
  18. theorem OAI.ArExplicit.TwoCone.cokernel_finite line 114
  19. theorem OAI.ArExplicit.TwoCone.d_apply line 119