OAI/Algebra/AuslanderReiten/Modules/TwistedBimodule.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.ArExplicit.TwistedBimodule line 11
2. def OAI.ArExplicit.TwistedBimodule.coordinates line 19
3. instance OAI.ArExplicit.TwistedBimodule.(instance at line 25) line 25
4. instance OAI.ArExplicit.TwistedBimodule.(instance at line 26) line 26
5. instance OAI.ArExplicit.TwistedBimodule.(instance at line 27) line 27
6. theorem OAI.ArExplicit.TwistedBimodule.value_zero line 29
7. theorem OAI.ArExplicit.TwistedBimodule.value_add line 30
8. theorem OAI.ArExplicit.TwistedBimodule.value_left_smul line 32
9. theorem OAI.ArExplicit.TwistedBimodule.value_scalar_smul line 34
10. instance OAI.ArExplicit.TwistedBimodule.(instance at line 37) line 37
11. theorem OAI.ArExplicit.TwistedBimodule.value_right_smul line 40
12. instance OAI.ArExplicit.TwistedBimodule.(instance at line 43) line 43
13. instance OAI.ArExplicit.TwistedBimodule.(instance at line 51) line 51
14. instance OAI.ArExplicit.TwistedBimodule.(instance at line 54) line 54
15. instance OAI.ArExplicit.TwistedBimodule.(instance at line 57) line 57
16. instance OAI.ArExplicit.TwistedBimodule.(instance at line 60) line 60
17. instance OAI.ArExplicit.TwistedBimodule.(instance at line 66) line 66
18. def OAI.ArExplicit.TwistedBimodule.leftLinearEquiv line 69
19. def OAI.ArExplicit.TwistedBimodule.rightLinearEquiv line 71
20. def OAI.ArExplicit.TwistedBimodule.scalarLinearEquiv line 82
21. instance OAI.ArExplicit.TwistedBimodule.(instance at line 84) line 84
22. instance OAI.ArExplicit.TwistedBimodule.(instance at line 87) line 87
23. instance OAI.ArExplicit.TwistedBimodule.(instance at line 90) line 90
24. instance OAI.ArExplicit.TwistedBimodule.(instance at line 93) line 93
25. instance OAI.ArExplicit.TwistedBimodule.(instance at line 96) line 96