OAI/Algebra/AuslanderReiten/Triangular/Triangular.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.ArExplicit.Triangular line 12
2. def OAI.ArExplicit.Triangular.coordinates line 21
3. instance OAI.ArExplicit.Triangular.(instance at line 27) line 27
4. def OAI.ArExplicit.Triangular.coordinateAddEquiv line 30
5. instance OAI.ArExplicit.Triangular.(instance at line 38) line 38
6. instance OAI.ArExplicit.Triangular.(instance at line 40) line 40
7. theorem OAI.ArExplicit.Triangular.top_zero line 48
8. theorem OAI.ArExplicit.Triangular.bottom_zero line 49
9. theorem OAI.ArExplicit.Triangular.off_zero line 50
10. theorem OAI.ArExplicit.Triangular.top_one line 51
11. theorem OAI.ArExplicit.Triangular.bottom_one line 52
12. theorem OAI.ArExplicit.Triangular.off_one line 53
13. theorem OAI.ArExplicit.Triangular.top_add line 54
14. theorem OAI.ArExplicit.Triangular.bottom_add line 55
15. theorem OAI.ArExplicit.Triangular.off_add line 57
16. theorem OAI.ArExplicit.Triangular.top_mul line 60
17. theorem OAI.ArExplicit.Triangular.bottom_mul line 61
18. theorem OAI.ArExplicit.Triangular.off_mul line 63
19. instance OAI.ArExplicit.Triangular.(instance at line 68) line 68
20. def OAI.ArExplicit.Triangular.diagonal line 84
21. theorem OAI.ArExplicit.Triangular.diagonal_surjective line 91
22. def OAI.ArExplicit.Triangular.offDiagonal line 95
23. theorem OAI.ArExplicit.Triangular.offDiagonal_mul_offDiagonal line 97
24. instance OAI.ArExplicit.Triangular.(instance at line 105) line 105
25. theorem OAI.ArExplicit.Triangular.top_smul line 107
26. theorem OAI.ArExplicit.Triangular.bottom_smul line 108
27. theorem OAI.ArExplicit.Triangular.off_smul line 110
28. instance OAI.ArExplicit.Triangular.(instance at line 115) line 115
29. def OAI.ArExplicit.Triangular.coordinateLinearEquiv line 132
30. instance OAI.ArExplicit.Triangular.(instance at line 135) line 135