OAI/Algebra/AuslanderReiten/Ext/ExtIsoFunctor.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.ArExplicit.selfExtIso_transline 15 - theorem
OAI.ArExplicit.selfExtIso_symm_applyline 20 - theorem
OAI.ArExplicit.selfExtIso_eqToIsoline 25 - theorem
OAI.ArExplicit.selfExtIso_mapExactFunctorline 32 - theorem
OAI.ArExplicit.selfExtIso_conjugated_functorline 38