OAI/Algebra/AuslanderReiten/Cones/TwoConeTailRestriction.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- abbrev
OAI.ArExplicit.TwoCone.restrictedSourceline 14 - def
OAI.ArExplicit.TwoCone.restrictedDifferentialline 16 - def
OAI.ArExplicit.TwoCone.restrictedHighLiftline 19 - theorem
OAI.ArExplicit.TwoCone.restrictedHighLift_commline 23