OAI/Algebra/AuslanderReiten/Cones/ConeEnd.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ArExplicit.coneEnd line 18
  2. def OAI.ArExplicit.coneEndA line 23
  3. def OAI.ArExplicit.coneEndB line 26
  4. def OAI.ArExplicit.coneEndC line 29
  5. def OAI.ArExplicit.coneEndUpper line 32
  6. theorem OAI.ArExplicit.coneEndA_mk line 35
  7. theorem OAI.ArExplicit.coneEndB_mk line 39
  8. theorem OAI.ArExplicit.coneEndC_mk line 43
  9. theorem OAI.ArExplicit.coneEndUpper_mk line 47
  10. theorem OAI.ArExplicit.coneEnd_ext line 51
  11. theorem OAI.ArExplicit.coneEnd_reconstruct line 59
  12. theorem OAI.ArExplicit.coneEnd_zero line 64
  13. theorem OAI.ArExplicit.coneEnd_eq_zero_iff line 68
  14. theorem OAI.ArExplicit.coneEnd_differential line 83
  15. theorem OAI.ArExplicit.coneEnd_closed_iff line 101
  16. theorem OAI.ArExplicit.coneEnd_all_reconstruct line 115
  17. theorem OAI.ArExplicit.coneEnd_boundary_iff line 121