OAI/Algebra/AuslanderReiten/Modules/BimoduleEnveloping.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ArExplicit.bimoduleEnvelopingRepresentation line 21
2. def OAI.ArExplicit.bimoduleEnvelopingModule line 28
3. def OAI.ArExplicit.bimoduleEnvelopingObject line 31
4. instance OAI.ArExplicit.(instance at line 35) line 35
5. instance OAI.ArExplicit.(instance at line 37) line 37
6. theorem OAI.ArExplicit.bimoduleEnveloping_smul line 44
7. def OAI.ArExplicit.bimoduleEnvelopingLeftEquiv line 47
8. def OAI.ArExplicit.bimoduleEnvelopingRightEquiv line 59