OAI/Algebra/AuslanderReiten/Triangular/TriangularModule.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.ArExplicit.TriangularModule line 14
2. def OAI.ArExplicit.TriangularModule.coordinates line 23
3. instance OAI.ArExplicit.TriangularModule.(instance at line 29) line 29
4. def OAI.ArExplicit.TriangularModule.coordinateAddEquiv line 31
5. theorem OAI.ArExplicit.TriangularModule.top_add line 35
6. theorem OAI.ArExplicit.TriangularModule.bottom_add line 36
7. theorem OAI.ArExplicit.TriangularModule.top_zero line 38
8. theorem OAI.ArExplicit.TriangularModule.bottom_zero line 39
9. instance OAI.ArExplicit.TriangularModule.(instance at line 41) line 41
10. theorem OAI.ArExplicit.TriangularModule.top_smul line 44
11. theorem OAI.ArExplicit.TriangularModule.bottom_smul line 46
12. instance OAI.ArExplicit.TriangularModule.(instance at line 49) line 49
13. instance OAI.ArExplicit.TriangularModule.(instance at line 69) line 69
14. theorem OAI.ArExplicit.TriangularModule.top_scalar line 71
15. theorem OAI.ArExplicit.TriangularModule.bottom_scalar line 73
16. instance OAI.ArExplicit.TriangularModule.(instance at line 80) line 80
17. instance OAI.ArExplicit.TriangularModule.(instance at line 87) line 87
18. def OAI.ArExplicit.TriangularModule.coordinateLinearEquiv line 95
19. instance OAI.ArExplicit.TriangularModule.(instance at line 98) line 98