OAI/Algebra/AuslanderReiten/Fibers/BimoduleFiber.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ArExplicit.twistedFiniteModule line 18
2. theorem OAI.ArExplicit.twistedFiniteModule_left line 24
3. theorem OAI.ArExplicit.twistedFiniteModule_right line 32
4. abbrev OAI.ArExplicit.BimoduleFiber.target line 44
5. abbrev OAI.ArExplicit.BimoduleFiber.finiteModule line 50
6. abbrev OAI.ArExplicit.BimoduleFiber.bimodule line 53
7. theorem OAI.ArExplicit.BimoduleFiber.target_left line 55
8. theorem OAI.ArExplicit.BimoduleFiber.target_right line 64
9. theorem OAI.ArExplicit.BimoduleFiber.left line 73
10. theorem OAI.ArExplicit.BimoduleFiber.right line 95