OAI/Algebra/AuslanderReiten/Cones/TwoConeRestriction.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.ArExplicit.TwoCone.Data.restrictline 14 - def
OAI.ArExplicit.TwoCone.termRestrictionEquivline 24 - def
OAI.ArExplicit.TwoCone.cokernelRestrictionEquivline 33 - theorem
OAI.ArExplicit.TwoCone.restricted_exactline 43 - theorem
OAI.ArExplicit.TwoCone.Cā_side_projectiveline 46