OAI/Algebra/AuslanderReiten/Tensor/TwistedTensor.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.ArExplicit.TwistedLeftModule line 8
2. def OAI.ArExplicit.TwistedLeftModule.coordinates line 19
3. instance OAI.ArExplicit.TwistedLeftModule.(instance at line 25) line 25
4. instance OAI.ArExplicit.TwistedLeftModule.(instance at line 26) line 26
5. instance OAI.ArExplicit.TwistedLeftModule.(instance at line 27) line 27
6. theorem OAI.ArExplicit.TwistedLeftModule.value_zero line 30
7. theorem OAI.ArExplicit.TwistedLeftModule.value_add line 32
8. theorem OAI.ArExplicit.TwistedLeftModule.value_scalar_smul line 35
9. theorem OAI.ArExplicit.TwistedLeftModule.value_smul line 38
10. instance OAI.ArExplicit.TwistedLeftModule.(instance at line 41) line 41
11. instance OAI.ArExplicit.TwistedLeftModule.(instance at line 49) line 49
12. instance OAI.ArExplicit.TwistedLeftModule.(instance at line 52) line 52
13. def OAI.ArExplicit.TwistedLeftModule.scalarEquiv line 55
14. instance OAI.ArExplicit.TwistedLeftModule.(instance at line 60) line 60
15. def OAI.ArExplicit.TwistedBimodule.untwistBilinear line 72
16. theorem OAI.ArExplicit.TwistedBimodule.untwist_balanced line 80
17. theorem OAI.ArExplicit.TwistedBimodule.untwist_left line 86
18. def OAI.ArExplicit.TwistedBimodule.tensorUntwistMap line 92
19. theorem OAI.ArExplicit.TwistedBimodule.tensorUntwistMap_tmul line 96
20. def OAI.ArExplicit.TwistedBimodule.untwistInverse line 99
21. def OAI.ArExplicit.TwistedBimodule.tensorUntwist line 103