OAI/Algebra/Finitistic/Ordinary/OrdinaryRetainedBimodule.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.RetainedBimodule line 9

   Source documentation

   An ordinary bimodule packaged as a module over its actual tensor algebra.

   def RetainedBimodule (_k _S _A M : Type u) := M
   …

2. instance OAI.LittleFinitistic.RetainedBimodule.(instance at line 14) line 14
3. instance OAI.LittleFinitistic.RetainedBimodule.(instance at line 15) line 15
4. instance OAI.LittleFinitistic.RetainedBimodule.(instance at line 16) line 16
5. instance OAI.LittleFinitistic.RetainedBimodule.(instance at line 17) line 17
6. instance OAI.LittleFinitistic.RetainedBimodule.(instance at line 18) line 18
7. instance OAI.LittleFinitistic.RetainedBimodule.(instance at line 19) line 19
8. instance OAI.LittleFinitistic.RetainedBimodule.(instance at line 20) line 20
9. def OAI.LittleFinitistic.RetainedBimodule.action line 23
10. instance OAI.LittleFinitistic.RetainedBimodule.(instance at line 29) line 29
11. instance OAI.LittleFinitistic.RetainedBimodule.tower line 30
12. def OAI.LittleFinitistic.RetainedBimodule.map line 40