OAI/Algebra/Finitistic/Ordinary/OrdinaryAssociativeTensorModules.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.RightTensor line 8

   Source documentation

   A tensor retaining the right action of the middle bimodule.

   def RightTensor (k A : Type u) (_ : Type u) (M N : Type u) [Field k] [Ring A] [Algebra k A]
       [AddCommGroup M] [Module k M] [Module Aᵐᵒᵖ M]
       [AddCommGroup N] [Module k N] [Module A N] := BalancedTensor.Tensor k A M N

   Mentions: OAI.LittleFinitistic.BalancedTensor.Tensor

2. def OAI.LittleFinitistic.LeftTensor line 13

   Source documentation

   A tensor retaining the left action of the middle bimodule.

   def LeftTensor (k B : Type u) (_ : Type u) (N Z : Type u) [Field k] [Ring B] [Algebra k B]
       [AddCommGroup N] [Module k N] [Module Bᵐᵒᵖ N]
       [AddCommGroup Z] [Module k Z] [Module B Z] := BalancedTensor.Tensor k B N Z
   …

   Mentions: OAI.LittleFinitistic.BalancedTensor.Tensor

3. instance OAI.LittleFinitistic.RightTensor.(instance at line 24) line 24
4. instance OAI.LittleFinitistic.RightTensor.(instance at line 25) line 25
5. def OAI.LittleFinitistic.RightTensor.action line 29
6. instance OAI.LittleFinitistic.RightTensor.(instance at line 31) line 31
7. instance OAI.LittleFinitistic.RightTensor.(instance at line 32) line 32
8. def OAI.LittleFinitistic.RightTensor.mk line 38
9. theorem OAI.LittleFinitistic.RightTensor.smul_mk line 41
10. instance OAI.LittleFinitistic.LeftTensor.(instance at line 46) line 46
11. instance OAI.LittleFinitistic.LeftTensor.(instance at line 47) line 47
12. def OAI.LittleFinitistic.LeftTensor.action line 49
13. instance OAI.LittleFinitistic.LeftTensor.(instance at line 50) line 50
14. instance OAI.LittleFinitistic.LeftTensor.(instance at line 51) line 51
15. def OAI.LittleFinitistic.LeftTensor.mk line 57
16. theorem OAI.LittleFinitistic.LeftTensor.smul_mk line 60