OAI/Algebra/AuslanderReiten/Modules/Coinduced.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.ArExplicit.Coinduced line 10
2. def OAI.ArExplicit.Coinduced.coordinates line 17
3. instance OAI.ArExplicit.Coinduced.(instance at line 23) line 23
4. instance OAI.ArExplicit.Coinduced.(instance at line 24) line 24
5. theorem OAI.ArExplicit.Coinduced.functional_zero line 26
6. theorem OAI.ArExplicit.Coinduced.functional_add line 27
7. theorem OAI.ArExplicit.Coinduced.functional_smul line 29
8. def OAI.ArExplicit.Coinduced.action line 32
9. instance OAI.ArExplicit.Coinduced.(instance at line 37) line 37
10. theorem OAI.ArExplicit.Coinduced.functional_action line 39
11. instance OAI.ArExplicit.Coinduced.(instance at line 42) line 42
12. instance OAI.ArExplicit.Coinduced.(instance at line 50) line 50
13. instance OAI.ArExplicit.Coinduced.(instance at line 53) line 53
14. def OAI.ArExplicit.Coinduced.scalarLinearEquiv line 56
15. def OAI.ArExplicit.Coinduced.evalOne line 59
16. def OAI.ArExplicit.Coinduced.fromFunctional line 64
17. instance OAI.ArExplicit.Coinduced.(instance at line 76) line 76
18. instance OAI.ArExplicit.Coinduced.(instance at line 91) line 91
19. theorem OAI.ArExplicit.Coinduced.finrank_eq line 94