OAI/Algebra/AuslanderReiten/Cones/TwoConeModuleTriangles.lean
12 declarations, 0 contain sorry, 0 declared as axioms
- abbrev
OAI.ArExplicit.TwoCone.termModuleline 16 - abbrev
OAI.ArExplicit.TwoCone.baseCokernelModuleline 22 - abbrev
OAI.ArExplicit.TwoCone.middleCokernelModuleline 28 - abbrev
OAI.ArExplicit.TwoCone.skeletonCokernelModuleline 34 - abbrev
OAI.ArExplicit.TwoCone.cokernelModuleline 43 - theorem
OAI.ArExplicit.TwoCone.exists_skeleton_triangleline 55 - theorem
OAI.ArExplicit.TwoCone.exists_top_triangleline 74 - def
OAI.ArExplicit.TwoCone.baseStepInclusionline 95 - theorem
OAI.ArExplicit.TwoCone.baseStepInclusion_injectiveline 99 - theorem
OAI.ArExplicit.TwoCone.baseStep_exactline 102 - def
OAI.ArExplicit.TwoCone.baseSuccessorShiftIsoline 112 - def
OAI.ArExplicit.TwoCone.baseIteratedShiftIsoline 122