OAI/Algebra/AuslanderReiten/Modules/InductionBimodule.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.ArExplicit.InductionBimodule line 10
2. def OAI.ArExplicit.InductionBimodule.coordinates line 18
3. instance OAI.ArExplicit.InductionBimodule.(instance at line 24) line 24
4. instance OAI.ArExplicit.InductionBimodule.(instance at line 25) line 25
5. instance OAI.ArExplicit.InductionBimodule.(instance at line 26) line 26
6. instance OAI.ArExplicit.InductionBimodule.(instance at line 27) line 27
7. theorem OAI.ArExplicit.InductionBimodule.value_zero line 29
8. theorem OAI.ArExplicit.InductionBimodule.value_add line 30
9. theorem OAI.ArExplicit.InductionBimodule.value_smul line 31
10. theorem OAI.ArExplicit.InductionBimodule.value_scalar line 32
11. theorem OAI.ArExplicit.InductionBimodule.value_right line 33
12. instance OAI.ArExplicit.InductionBimodule.(instance at line 36) line 36
13. instance OAI.ArExplicit.InductionBimodule.(instance at line 44) line 44
14. instance OAI.ArExplicit.InductionBimodule.(instance at line 46) line 46
15. instance OAI.ArExplicit.InductionBimodule.(instance at line 48) line 48
16. instance OAI.ArExplicit.InductionBimodule.(instance at line 50) line 50
17. instance OAI.ArExplicit.InductionBimodule.(instance at line 55) line 55
18. def OAI.ArExplicit.InductionBimodule.leftEquiv line 58
19. def OAI.ArExplicit.InductionBimodule.scalarEquiv line 59
20. instance OAI.ArExplicit.InductionBimodule.(instance at line 61) line 61
21. instance OAI.ArExplicit.InductionBimodule.(instance at line 62) line 62
22. instance OAI.ArExplicit.InductionBimodule.(instance at line 63) line 63