OAI/Algebra/Finitistic/Ordinary/OrdinaryBlockModules.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.BlockModule.First line 9

   Source documentation

   A module supported on the first factor of the actual product algebra.

   def First (_k _L _R Z : Type u) := Z

2. def OAI.LittleFinitistic.BlockModule.Second line 11

   Source documentation

   A module supported on the second factor of the actual product algebra.

   def Second (_k _L _R Z : Type u) := Z
   …

3. instance OAI.LittleFinitistic.BlockModule.First.(instance at line 15) line 15
4. instance OAI.LittleFinitistic.BlockModule.First.(instance at line 16) line 16
5. instance OAI.LittleFinitistic.BlockModule.First.(instance at line 17) line 17
6. instance OAI.LittleFinitistic.BlockModule.First.(instance at line 18) line 18
7. instance OAI.LittleFinitistic.BlockModule.Second.(instance at line 22) line 22
8. instance OAI.LittleFinitistic.BlockModule.Second.(instance at line 23) line 23
9. instance OAI.LittleFinitistic.BlockModule.Second.(instance at line 24) line 24
10. instance OAI.LittleFinitistic.BlockModule.Second.(instance at line 25) line 25