OAI/Algebra/AuslanderReiten/Tensor/EnvelopingBimodule.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.ArExplicit.EnvelopingBimodule line 15
2. def OAI.ArExplicit.EnvelopingBimodule.coordinates line 24
3. instance OAI.ArExplicit.EnvelopingBimodule.(instance at line 30) line 30
4. instance OAI.ArExplicit.EnvelopingBimodule.(instance at line 31) line 31
5. instance OAI.ArExplicit.EnvelopingBimodule.(instance at line 33) line 33
6. instance OAI.ArExplicit.EnvelopingBimodule.(instance at line 35) line 35
7. theorem OAI.ArExplicit.EnvelopingBimodule.value_zero line 38
8. theorem OAI.ArExplicit.EnvelopingBimodule.value_add line 39
9. theorem OAI.ArExplicit.EnvelopingBimodule.value_smul line 41
10. theorem OAI.ArExplicit.EnvelopingBimodule.value_left_smul line 43
11. theorem OAI.ArExplicit.EnvelopingBimodule.value_right_smul line 45
12. instance OAI.ArExplicit.EnvelopingBimodule.(instance at line 48) line 48
13. def OAI.ArExplicit.EnvelopingBimodule.leftEquiv line 55
14. def OAI.ArExplicit.EnvelopingBimodule.rightEquiv line 61
15. instance OAI.ArExplicit.EnvelopingBimodule.(instance at line 67) line 67
16. instance OAI.ArExplicit.EnvelopingBimodule.(instance at line 71) line 71
17. instance OAI.ArExplicit.EnvelopingBimodule.(instance at line 75) line 75
18. instance OAI.ArExplicit.EnvelopingBimodule.(instance at line 79) line 79
19. instance OAI.ArExplicit.EnvelopingBimodule.(instance at line 85) line 85
20. theorem OAI.ArExplicit.EnvelopingBimodule.value_scalar_smul line 87
21. def OAI.ArExplicit.EnvelopingBimodule.scalarEquiv line 90
22. instance OAI.ArExplicit.EnvelopingBimodule.(instance at line 92) line 92
23. instance OAI.ArExplicit.EnvelopingBimodule.(instance at line 97) line 97
24. instance OAI.ArExplicit.EnvelopingBimodule.(instance at line 103) line 103
25. instance OAI.ArExplicit.EnvelopingBimodule.(instance at line 111) line 111
26. instance OAI.ArExplicit.EnvelopingBimodule.(instance at line 115) line 115