OAI/Algebra/AuslanderReiten/Tensor/EnvelopingBalancedExact.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.ArExplicit.EnvelopingBimodule.mapRightline 19 - theorem
OAI.ArExplicit.EnvelopingBimodule.mapRight_injectiveline 25 - theorem
OAI.ArExplicit.EnvelopingBimodule.mapRight_surjectiveline 32 - theorem
OAI.ArExplicit.EnvelopingBimodule.mapRight_exactline 40 - theorem
OAI.ArExplicit.EnvelopingBimodule.mapFirst_mapRight_applyline 61 - theorem
OAI.ArExplicit.EnvelopingBimodule.tensorMap_shortExactline 65