OAI/Algebra/AuslanderReiten/Duality/RightDual.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.ArExplicit.RightDual line 9
2. def OAI.ArExplicit.RightDual.coordinates line 19
3. instance OAI.ArExplicit.RightDual.(instance at line 25) line 25
4. instance OAI.ArExplicit.RightDual.(instance at line 26) line 26
5. theorem OAI.ArExplicit.RightDual.functional_zero line 29
6. theorem OAI.ArExplicit.RightDual.functional_add line 31
7. theorem OAI.ArExplicit.RightDual.functional_smul line 34
8. def OAI.ArExplicit.RightDual.scalarEquiv line 37
9. instance OAI.ArExplicit.RightDual.(instance at line 40) line 40
10. theorem OAI.ArExplicit.RightDual.functional_action line 46
11. instance OAI.ArExplicit.RightDual.(instance at line 49) line 49
12. instance OAI.ArExplicit.RightDual.(instance at line 57) line 57
13. instance OAI.ArExplicit.RightDual.(instance at line 59) line 59
14. def OAI.ArExplicit.RightDual.map line 62
15. theorem OAI.ArExplicit.RightDual.map_apply line 67
16. theorem OAI.ArExplicit.RightDual.map_comp line 70
17. def OAI.ArExplicit.RightDual.congr line 73
18. theorem OAI.ArExplicit.RightDual.map_exact line 87
19. theorem OAI.ArExplicit.RightDual.map_surjective line 105