OAI/Algebra/AuslanderReiten/Homology/TriangleRecurrence.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.ArExplicit.TriangleRecurrence.connecting_surjectiveline 17 - theorem
OAI.ArExplicit.TriangleRecurrence.connecting_injectiveline 23 - theorem
OAI.ArExplicit.TriangleRecurrence.connecting_bijectiveline 37 - def
OAI.ArExplicit.TriangleRecurrence.connectingEquivline 43 - def
OAI.ArExplicit.TriangleRecurrence.shiftedMapEquivline 56 - theorem
OAI.ArExplicit.TriangleRecurrence.degreeThreeComposition_bijectiveline 63