OAI/Algebra/AuslanderReiten/Modules/CoinducedModule.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.ArExplicit.CoinducedModule line 10
2. def OAI.ArExplicit.CoinducedModule.coordinates line 19
3. instance OAI.ArExplicit.CoinducedModule.(instance at line 25) line 25
4. instance OAI.ArExplicit.CoinducedModule.(instance at line 26) line 26
5. theorem OAI.ArExplicit.CoinducedModule.functional_zero line 28
6. theorem OAI.ArExplicit.CoinducedModule.functional_add line 29
7. theorem OAI.ArExplicit.CoinducedModule.functional_smul line 31
8. instance OAI.ArExplicit.CoinducedModule.(instance at line 34) line 34
9. theorem OAI.ArExplicit.CoinducedModule.functional_action line 39
10. instance OAI.ArExplicit.CoinducedModule.(instance at line 42) line 42
11. instance OAI.ArExplicit.CoinducedModule.(instance at line 50) line 50
12. instance OAI.ArExplicit.CoinducedModule.(instance at line 53) line 53
13. def OAI.ArExplicit.CoinducedModule.scalarEquiv line 56
14. instance OAI.ArExplicit.CoinducedModule.(instance at line 59) line 59
15. def OAI.ArExplicit.CoinducedModule.embedding line 66
16. theorem OAI.ArExplicit.CoinducedModule.embedding_apply line 73
17. theorem OAI.ArExplicit.CoinducedModule.embedding_injective line 76
18. def OAI.ArExplicit.CoinducedModule.coefficients line 85
19. def OAI.ArExplicit.CoinducedModule.coordinateEquiv line 88
20. def OAI.ArExplicit.CoinducedModule.freeEquiv line 105
21. theorem OAI.ArExplicit.CoinducedModule.finite line 109
22. theorem OAI.ArExplicit.CoinducedModule.free line 112
23. theorem OAI.ArExplicit.CoinducedModule.projective line 115