OAI/Algebra/AuslanderReiten/Cones/TwoConeConnectingMaps.lean
9 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.ArExplicit.TwoCone.firstCokernelMapline 11 - def
OAI.ArExplicit.TwoCone.secondCokernelMapline 18 - theorem
OAI.ArExplicit.TwoCone.firstCokernelMap_mkline 26 - theorem
OAI.ArExplicit.TwoCone.secondCokernelMap_mkline 30 - def
OAI.ArExplicit.TwoCone.rowCokernelMapline 33 - def
OAI.ArExplicit.TwoCone.columnCokernelMapline 37 - def
OAI.ArExplicit.TwoCone.topAttachingCokernelline 41 - theorem
OAI.ArExplicit.TwoCone.topAttachingCokernel_mkline 53 - theorem
OAI.ArExplicit.TwoCone.topAttachingCokernel_adjacentline 57