OAI/Algebra/AuslanderReiten/Complete/FiniteCompleteResolution.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.ArExplicit.FiniteLeftModule line 16
  2. structure OAI.ArExplicit.FiniteLeftModule.FreeCover line 28
  3. def OAI.ArExplicit.FiniteLeftModule.cover line 33
  4. def OAI.ArExplicit.FiniteLeftModule.syzygy line 38
  5. def OAI.ArExplicit.FiniteLeftModule.syzygies line 45
  6. def OAI.ArExplicit.FiniteLeftModule.envelopeRank line 49
  7. def OAI.ArExplicit.FiniteLeftModule.envelopeMap line 52
  8. theorem OAI.ArExplicit.FiniteLeftModule.envelopeMap_injective line 55
  9. def OAI.ArExplicit.FiniteLeftModule.cosyzygy line 58
  10. def OAI.ArExplicit.FiniteLeftModule.cosyzygies line 65
  11. abbrev OAI.ArExplicit.FiniteLeftModule.positiveTerm line 70
  12. def OAI.ArExplicit.FiniteLeftModule.positiveDifferential line 73
  13. theorem OAI.ArExplicit.FiniteLeftModule.positiveDifferential_range line 77
  14. theorem OAI.ArExplicit.FiniteLeftModule.positiveDifferential_kernel line 87
  15. theorem OAI.ArExplicit.FiniteLeftModule.positiveDifferential_exact line 93
  16. abbrev OAI.ArExplicit.FiniteLeftModule.negativeTerm line 98
  17. def OAI.ArExplicit.FiniteLeftModule.negativeDifferential line 101
  18. theorem OAI.ArExplicit.FiniteLeftModule.negativeDifferential_range line 107
  19. theorem OAI.ArExplicit.FiniteLeftModule.negativeDifferential_kernel line 120
  20. theorem OAI.ArExplicit.FiniteLeftModule.negativeDifferential_exact line 130
  21. def OAI.ArExplicit.FiniteLeftModule.seam line 136
  22. theorem OAI.ArExplicit.FiniteLeftModule.seam_range line 140
  23. theorem OAI.ArExplicit.FiniteLeftModule.seam_kernel line 150
  24. def OAI.ArExplicit.FiniteLeftModule.term line 155
  25. def OAI.ArExplicit.FiniteLeftModule.differential line 159
  26. theorem OAI.ArExplicit.FiniteLeftModule.adjacent_exact line 165
  27. theorem OAI.ArExplicit.FiniteLeftModule.differential_square line 184
  28. def OAI.ArExplicit.FiniteLeftModule.completeComplex line 189
  29. theorem OAI.ArExplicit.FiniteLeftModule.completeComplex_exact line 193
  30. theorem OAI.ArExplicit.FiniteLeftModule.completeComplex_exactProjective line 204
  31. theorem OAI.ArExplicit.FiniteLeftModule.completeComplex_totallyAcyclic line 216
  32. def OAI.ArExplicit.FiniteLeftModule.completeCokernelEquiv line 221
  33. theorem OAI.ArExplicit.exists_finite_complete_resolution line 229